let F, G be ZF-formula; :: 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 )
('not' F) '&' ('not' G) is_immediate_constituent_of F 'or' G by ZF_LANG:def 39;
hence A1: ('not' F) '&' ('not' G) is_proper_subformula_of F 'or' G by ZF_LANG:82; :: 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_immediate_constituent_of ('not' F) '&' ('not' G) & 'not' G is_immediate_constituent_of ('not' F) '&' ('not' G) ) by ZF_LANG:def 39;
hence A2: ( 'not' F is_proper_subformula_of F 'or' G & 'not' G is_proper_subformula_of F 'or' G ) by A1, Th44; :: thesis: ( F is_proper_subformula_of F 'or' G & G is_proper_subformula_of F 'or' G )
( F is_immediate_constituent_of 'not' F & G is_immediate_constituent_of 'not' G ) by ZF_LANG:def 39;
hence ( F is_proper_subformula_of F 'or' G & G is_proper_subformula_of F 'or' G ) by A2, Th44; :: thesis: verum