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