theorem Th4: :: LUKASI_1:4

for A being QC-alphabet
for p being Element of CQC-WFF A holds p => p in TAUT A