set X = { S where S is Element of QC-Sub-WFF : S `1 is Element of CQC-WFF } ;
{ S where S is Element of QC-Sub-WFF : S `1 is Element of CQC-WFF } c= QC-Sub-WFF

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in { S where S is Element of QC-Sub-WFF : S `1 is Element of CQC-WFF } or a in QC-Sub-WFF )
assume a in { S where S is Element of QC-Sub-WFF : S `1 is Element of CQC-WFF } ; :: thesis: a in QC-Sub-WFF
then ex S being Element of QC-Sub-WFF st
( a = S & S `1 is Element of CQC-WFF ) ;
hence a in QC-Sub-WFF ; :: thesis: verum

end;

hence { S where S is Element of QC-Sub-WFF : S `1 is Element of CQC-WFF } is Subset of QC-Sub-WFF ; :: thesis: verum