let F, G be ZF-formula; :: thesis: ( F '&' ('not' G) is_proper_subformula_of F => G & F is_proper_subformula_of F => G & 'not' G is_proper_subformula_of F => G & G is_proper_subformula_of F => G )
F '&' ('not' G) is_immediate_constituent_of F => G ;
hence A1: F '&' ('not' G) is_proper_subformula_of F => G by ZF_LANG:61; :: thesis: ( F is_proper_subformula_of F => G & 'not' G is_proper_subformula_of F => G & G is_proper_subformula_of F => G )
( F is_immediate_constituent_of F '&' ('not' G) & 'not' G is_immediate_constituent_of F '&' ('not' G) ) ;
hence A2: ( F is_proper_subformula_of F => G & 'not' G is_proper_subformula_of F => G ) by A1, Th40; :: thesis: G is_proper_subformula_of F => G
G is_immediate_constituent_of 'not' G ;
hence G is_proper_subformula_of F => G by A2, Th40; :: thesis: verum