let H be Element of QC-WFF ; :: thesis: ( H is biconditional implies H = (the_left_side_of H) <=> (the_right_side_of H) )
given F, G being Element of QC-WFF such that A1: H = F <=> G ; :: according to QC_LANG2:def 12 :: thesis: H = (the_left_side_of H) <=> (the_right_side_of H)
( the_left_side_of H = F & the_right_side_of H = G ) by A1, Th47;
hence H = (the_left_side_of H) <=> (the_right_side_of H) by A1; :: thesis: verum