theorem :: QC_LANG2:9

for A being QC-alphabet
for p, q being Element of QC-WFF A holds p 'or' q = ('not' p) => q ;