let H be Element of QC-WFF ; :: thesis: ( H is conditional implies H = (the_antecedent_of H) => (the_consequent_of H) )
given F, G being Element of QC-WFF 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, Th46;
hence H = (the_antecedent_of H) => (the_consequent_of H) by A1, Th46; :: thesis: verum