theorem :: ZF_LANG1:27

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