let A be QC-alphabet ; :: thesis: for F, G being Element of QC-WFF A holds
( ('not' F) '&' ('not' G) is_proper_subformula_of F 'or' G & 'not' F is_proper_subformula_of F 'or' G & 'not' G is_proper_subformula_of F 'or' G & F is_proper_subformula_of F 'or' G & G is_proper_subformula_of F 'or' G )
let F, G be Element of QC-WFF A; :: thesis: ( ('not' F) '&' ('not' G) is_proper_subformula_of F 'or' G & 'not' F is_proper_subformula_of F 'or' G & 'not' G is_proper_subformula_of F 'or' G & F is_proper_subformula_of F 'or' G & G is_proper_subformula_of F 'or' G )
thus A1: ('not' F) '&' ('not' G) is_proper_subformula_of F 'or' G by Th66; :: thesis: ( 'not' F is_proper_subformula_of F 'or' G & 'not' G is_proper_subformula_of F 'or' G & F is_proper_subformula_of F 'or' G & G is_proper_subformula_of F 'or' G )
( 'not' F is_proper_subformula_of ('not' F) '&' ('not' G) & 'not' G is_proper_subformula_of ('not' F) '&' ('not' G) ) by Th69;
hence A2: ( 'not' F is_proper_subformula_of F 'or' G & 'not' G is_proper_subformula_of F 'or' G ) by A1, Th56; :: thesis: ( F is_proper_subformula_of F 'or' G & G is_proper_subformula_of F 'or' G )
( G is_proper_subformula_of 'not' G & F is_proper_subformula_of 'not' F ) by Th66;
hence ( F is_proper_subformula_of F 'or' G & G is_proper_subformula_of F 'or' G ) by A2, Th56; :: thesis: verum