:: deftheorem defines biconditional QC_LANG2:def 12 :
for A being QC-alphabet
for H being Element of QC-WFF A holds
( H is biconditional iff ex p, q being Element of QC-WFF A st H = p <=> q );