let F, G be Element of QC-WFF ; :: 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 Th2
.= F by Th5 ; :: 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 Th2
.= the_argument_of ('not' G) by Th5
.= G by Th2 ; :: thesis: the_argument_of (F => G) = F '&' ('not' G)
thus the_argument_of (F => G) = F '&' ('not' G) by Th2; :: thesis: verum