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