let p, q be ZF-formula; :: thesis: ( the_left_side_of (p <=> q) = p & the_right_side_of (p <=> q) = q )
p <=> q is biconditional ;
then p <=> q = (the_left_side_of (p <=> q)) <=> (the_right_side_of (p <=> q)) by ZF_LANG:49;
hence ( the_left_side_of (p <=> q) = p & the_right_side_of (p <=> q) = q ) by ZF_LANG:33; :: thesis: verum