for A being QC-alphabet
for H being Element of QC-WFF A st H is biconditional holds
H = (the_left_side_of H) <=> (the_right_side_of H)