let F, H 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) ;
hence ( All (x,H) is_subformula_of F implies H is_proper_subformula_of F ) by Th40; :: thesis: verum