вывести в ГИВ

[Dina92]

помогите вывести формулу $ F \lor \neg F $ в гильбертовском исчислении высказываний, с аксиомами:
1. $ A \to (B \to A) $
2. $ (A \to B) \to ((A \to (B \to C)) \to (A \to C)) $
3. $ (A \land B) \to A $
4. $ (A \land B) \to B $
5. $ (C \to A) \to ((C \to B) \to (C \to (A \land B))) $
6. $ A \to (A \lor B) $
7. $ B \to (A \lor B) $
8. $ (A \to C) \to ((B \to C) \to ((A \lor B) \to C)) $
9. $ ((A \to \neg B) \to (B \to \neg A)) $
10. $ \neg \neg A \to A $

и правилом вывода: $ \cfrac{A, A \to B}{B} $
можно использовать теорему о дедукции: если $H, A \vdash B$, то $H \vdash A \to B$