theorem Th3: :: PROCAL_1:3

for A being QC-alphabet
for p, q being Element of CQC-WFF A holds p => (p 'or' q) in TAUT A