theorem Th30: :: ZF_LANG:30

for G, G1, H, H1 being ZF-formula st H '&' G = H1 '&' G1 holds
( H = H1 & G = G1 )