:: deftheorem defines biconditional ZF_LANG:def 22 :
for H being ZF-formula holds
( H is biconditional iff ex F, G being ZF-formula st H = F <=> G );