theorem Th7: :: CQC_THE3:7

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