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