let x, y be Variable; :: thesis: for F being ZF-formula holds not F is_proper_subformula_of x 'in' y
let F be ZF-formula; :: thesis: not F is_proper_subformula_of x 'in' y
assume F is_proper_subformula_of x 'in' y ; :: thesis: contradiction
then ex G being ZF-formula st G is_immediate_constituent_of x 'in' y by Th63;
hence contradiction by Th51; :: thesis: verum