theorem Th31: :: ZF_LANG:31

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