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