:: deftheorem defines <=> QC_LANG2:def 4 :
for A being QC-alphabet
for p, q being Element of QC-WFF A holds p <=> q = (p => q) '&' (q => p);