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