let A be QC-alphabet ; :: thesis: for F, G being Element of QC-WFF A holds
( the_antecedent_of (F => G) = F & the_consequent_of (F => G) = G & the_argument_of (F => G) = F '&' ('not' G) )
let F, G be Element of QC-WFF A; :: thesis: ( the_antecedent_of (F => G) = F & the_consequent_of (F => G) = G & the_argument_of (F => G) = F '&' ('not' G) )
thus the_antecedent_of (F => G) = the_left_argument_of (F '&' ('not' G)) by Th1
.= F by Th4 ; :: thesis: ( the_consequent_of (F => G) = G & the_argument_of (F => G) = F '&' ('not' G) )
thus the_consequent_of (F => G) = the_argument_of (the_right_argument_of (F '&' ('not' G))) by Th1
.= the_argument_of ('not' G) by Th4
.= G by Th1 ; :: thesis: the_argument_of (F => G) = F '&' ('not' G)
thus the_argument_of (F => G) = F '&' ('not' G) by Th1; :: thesis: verum