let H be ZF-formula; :: thesis: ( H is biconditional implies ( H is conjunctive & the_left_argument_of H is conditional & the_right_argument_of H is conditional ) )
assume H is biconditional ; :: thesis: ( H is conjunctive & the_left_argument_of H is conditional & the_right_argument_of H is conditional )
then A1: H = (the_left_side_of H) <=> (the_right_side_of H) by ZF_LANG:49;
hence H is conjunctive by ZF_LANG:5; :: thesis: ( the_left_argument_of H is conditional & the_right_argument_of H is conditional )
( the_left_argument_of H = (the_left_side_of H) => (the_right_side_of H) & the_right_argument_of H = (the_right_side_of H) => (the_left_side_of H) ) by A1, Th4;
hence ( the_left_argument_of H is conditional & the_right_argument_of H is conditional ) by ZF_LANG:6; :: thesis: verum