let A be QC-alphabet ; :: thesis: for X being Subset of (CQC-WFF A) holds X |- X
let X be Subset of (CQC-WFF A); :: thesis: X |- X
for p being Element of CQC-WFF A st p in X holds
X |- p by Th1;
hence X |- X by Def2; :: thesis: verum