let x, y be Variable; :: thesis: for H being ZF-formula holds
( H is_subformula_of x 'in' y iff H = x 'in' y )
let H be ZF-formula; :: thesis: ( H is_subformula_of x 'in' y iff H = x 'in' y )
thus ( H is_subformula_of x 'in' y implies H = x 'in' y ) :: thesis: ( H = x 'in' y implies H is_subformula_of x 'in' y )

proof

assume A1: H is_subformula_of x 'in' y ; :: thesis: H = x 'in' y
assume H <> x 'in' y ; :: thesis: contradiction
then H is_proper_subformula_of x 'in' y by A1;
then ex F being ZF-formula st F is_immediate_constituent_of x 'in' y by Th63;
hence contradiction by Th51; :: thesis: verum

end;

assume H = x 'in' y ; :: thesis: H is_subformula_of x 'in' y
hence H is_subformula_of x 'in' y by Th59; :: thesis: verum