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

proof

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

end;

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