:: deftheorem Def35 defines the_antecedent_of ZF_LANG:def 35 :
for H being ZF-formula st H is conditional holds
for b₂ being ZF-formula holds
( b₂ = the_antecedent_of H iff ex H1 being ZF-formula st H = b₂ => H1 );