:: deftheorem defines <=> ZF_LANG:def 18 :
for F, G being ZF-formula holds F <=> G = (F => G) '&' (G => F);