let H be ZF-formula; :: thesis: ( H is conditional implies H = (the_antecedent_of H) => (the_consequent_of H) )
assume A1: H is conditional ; :: thesis: H = (the_antecedent_of H) => (the_consequent_of H)
then ex F being ZF-formula st H = (the_antecedent_of H) => F by Def35;
hence H = (the_antecedent_of H) => (the_consequent_of H) by A1, Def36; :: thesis: verum