theorem :: ZF_LANG1:30

for F, G being ZF-formula holds
( the_argument_of (F 'or' G) = ('not' F) '&' ('not' G) & the_antecedent_of (F 'or' G) = 'not' F & the_consequent_of (F 'or' G) = G )