let G, H be ZF-formula; :: thesis: ( not G is_proper_subformula_of H or not H is_proper_subformula_of G )
assume ( G is_proper_subformula_of H & H is_proper_subformula_of G ) ; :: thesis: contradiction
then G is_proper_subformula_of G by ZF_LANG:64;
hence contradiction ; :: thesis: verum