theorem Th32: :: ZF_LANG:32

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