let A be QC-alphabet ; :: thesis: for H being Element of QC-WFF A st H is conditional holds
( H is negative & the_argument_of H is conjunctive & the_right_argument_of (the_argument_of H) is negative )
let H be Element of QC-WFF A; :: thesis: ( H is conditional implies ( H is negative & the_argument_of H is conjunctive & the_right_argument_of (the_argument_of H) is negative ) )
given F, G being Element of QC-WFF A such that A1: H = F => G ; :: according to QC_LANG2:def 11 :: thesis: ( H is negative & the_argument_of H is conjunctive & the_right_argument_of (the_argument_of H) is negative )
( the_argument_of ('not' (F '&' ('not' G))) = F '&' ('not' G) & the_right_argument_of (F '&' ('not' G)) = 'not' G ) by Th1, Th4;
hence ( H is negative & the_argument_of H is conjunctive & the_right_argument_of (the_argument_of H) is negative ) by A1; :: thesis: verum