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

proof

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

end;

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