:: deftheorem Def38 defines the_right_side_of ZF_LANG:def 38 :
for H being ZF-formula st H is biconditional holds
for b₂ being ZF-formula holds
( b₂ = the_right_side_of H iff ex H1 being ZF-formula st H = H1 <=> b₂ );