set F = { s where s is QC-formula : ( Fixed s = {} & Free s = {} ) } ;
{ s where s is QC-formula : ( Fixed s = {} & Free s = {} ) } c= QC-WFF

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { s where s is QC-formula : ( Fixed s = {} & Free s = {} ) } or x in QC-WFF )
assume x in { s where s is QC-formula : ( Fixed s = {} & Free s = {} ) } ; :: thesis: x in QC-WFF
then ex s being QC-formula st
( s = x & Fixed s = {} & Free s = {} ) ;
hence x in QC-WFF ; :: thesis: verum

end;

hence { s where s is QC-formula : ( Fixed s = {} & Free s = {} ) } is Subset of QC-WFF ; :: thesis: verum