let H, F be ZF-formula; :: thesis: for x being Variable st All x,H is_subformula_of F holds
H is_proper_subformula_of F
let x be Variable; :: thesis: ( All x,H is_subformula_of F implies H is_proper_subformula_of F )
H is_immediate_constituent_of All x,H by ZF_LANG:def 39;
hence ( All x,H is_subformula_of F implies H is_proper_subformula_of F ) by Th44; :: thesis: verum