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 consider S being Element of QC-Sub-WFF such that
A1: ( a = S & S `1 is Element of CQC-WFF ) ;
thus a in QC-Sub-WFF by A1; :: 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