theorem Th5: :: CQC_THE3:5

for A being QC-alphabet
for p being Element of CQC-WFF A holds p |- p by CQC_THE2:87;