for H being ZF-formula st H is biconditional holds
( the_right_side_of H = the_consequent_of (the_left_argument_of H) & the_right_side_of H = the_antecedent_of (the_right_argument_of H) )