let F, G be ZF-formula; :: thesis: ( 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 )
thus the_argument_of (F 'or' G) = ('not' F) '&' ('not' G) by Th3; :: thesis: ( the_antecedent_of (F 'or' G) = 'not' F & the_consequent_of (F 'or' G) = G )
F 'or' G = ('not' F) => G ;
hence ( the_antecedent_of (F 'or' G) = 'not' F & the_consequent_of (F 'or' G) = G ) by Th6; :: thesis: verum