let H be ZF-formula; :: thesis: for x being Variable holds
( All (x,('not' H)) is_proper_subformula_of Ex (x,H) & 'not' H is_proper_subformula_of Ex (x,H) )
let x be Variable; :: thesis: ( All (x,('not' H)) is_proper_subformula_of Ex (x,H) & 'not' H is_proper_subformula_of Ex (x,H) )
All (x,('not' H)) is_immediate_constituent_of Ex (x,H) ;
hence A1: All (x,('not' H)) is_proper_subformula_of Ex (x,H) by ZF_LANG:61; :: thesis: 'not' H is_proper_subformula_of Ex (x,H)
'not' H is_immediate_constituent_of All (x,('not' H)) ;
hence 'not' H is_proper_subformula_of Ex (x,H) by A1, Th40; :: thesis: verum