theorem :: ZF_LANG:49

for H being ZF-formula st H is biconditional holds
H = (the_left_side_of H) <=> (the_right_side_of H)