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