let A be QC-alphabet ; :: thesis: for H being Element of QC-WFF A st H is conditional holds
H = (the_antecedent_of H) => (the_consequent_of H)
let H be Element of QC-WFF A; :: thesis: ( H is conditional implies H = (the_antecedent_of H) => (the_consequent_of H) )
given F, G being Element of QC-WFF A such that A1: H = F => G ; :: according to QC_LANG2:def 11 :: thesis: H = (the_antecedent_of H) => (the_consequent_of H)
the_antecedent_of H = F by A1, Th30;
hence H = (the_antecedent_of H) => (the_consequent_of H) by A1, Th30; :: thesis: verum