theorem :: ZF_LANG1:7

for p, q being ZF-formula holds
( the_left_side_of (p <=> q) = p & the_right_side_of (p <=> q) = q )