let A be QC-alphabet ; :: thesis: for F, G being Element of QC-WFF A holds
( 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) )
let F, G be Element of QC-WFF A; :: 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 Th1
.= the_argument_of ('not' F) by Th4
.= F by Th1 ; :: 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 Th1
.= the_argument_of ('not' G) by Th4
.= G by Th1 ; :: thesis: the_argument_of (F 'or' G) = ('not' F) '&' ('not' G)
thus the_argument_of (F 'or' G) = ('not' F) '&' ('not' G) by Th1; :: thesis: verum