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 by ZF_LANG:def 39;
hence A1: All x,('not' H) is_proper_subformula_of Ex x,H by ZF_LANG:82; :: thesis: 'not' H is_proper_subformula_of Ex x,H
'not' H is_immediate_constituent_of All x,('not' H) by ZF_LANG:def 39;
hence 'not' H is_proper_subformula_of Ex x,H by A1, Th44; :: thesis: verum