set X = { (a at f) where a is quasi-adjective of C : a in A } ;
{ (a at f) where a is quasi-adjective of C : a in A } c= QuasiAdjs C

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (a at f) where a is quasi-adjective of C : a in A } or x in QuasiAdjs C )
assume x in { (a at f) where a is quasi-adjective of C : a in A } ; :: thesis: x in QuasiAdjs C
then ex a being quasi-adjective of C st
( x = a at f & a in A ) ;
hence x in QuasiAdjs C ; :: thesis: verum

end;

hence { (a at f) where a is quasi-adjective of C : a in A } is Subset of (QuasiAdjs C) ; :: thesis: verum