theorem Th33: :: ZF_LANG:33

for F, F1, G, G1 being ZF-formula st F <=> G = F1 <=> G1 holds
( F = F1 & G = G1 )