theorem Th31: :: QC_LANG2:31

for A being QC-alphabet
for F, G being Element of QC-WFF A holds
( the_left_side_of (F <=> G) = F & the_right_side_of (F <=> G) = G & the_left_argument_of (F <=> G) = F => G & the_right_argument_of (F <=> G) = G => F )