theorem :: ZF_LANG:66

for G, H being ZF-formula st G is_subformula_of H & H is_subformula_of G holds
G = H