let F, G be Element of QC-WFF ; :: thesis: ( the_left_disjunct_of (F 'or' G) = F & the_right_disjunct_of (F 'or' G) = G & the_argument_of (F 'or' G) = ('not' F) '&' ('not' G) )
thus the_left_disjunct_of (F 'or' G) = the_argument_of (the_left_argument_of (('not' F) '&' ('not' G))) by Th2
.= the_argument_of ('not' F) by Th5
.= F by Th2 ; :: thesis: ( the_right_disjunct_of (F 'or' G) = G & the_argument_of (F 'or' G) = ('not' F) '&' ('not' G) )
thus the_right_disjunct_of (F 'or' G) = the_argument_of (the_right_argument_of (('not' F) '&' ('not' G))) by Th2
.= the_argument_of ('not' G) by Th5
.= G by Th2 ; :: thesis: the_argument_of (F 'or' G) = ('not' F) '&' ('not' G)
thus the_argument_of (F 'or' G) = ('not' F) '&' ('not' G) by Th2; :: thesis: verum