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