theorem :: CQC_THE3:17

for A being QC-alphabet
for X being Subset of (CQC-WFF A) holds
( |- X iff X c= TAUT A )