defpred S₁[ set ] means for a being adjective of T st a in A holds
$1 in types a;
consider tt being set such that
A1: for x being set holds
( x in tt iff ( x in the carrier of T & S₁[x] ) ) from XBOOLE_0:sch 1();
tt c= the carrier of T

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in tt or x in the carrier of T )
thus ( not x in tt or x in the carrier of T ) by A1; :: thesis: verum

end;

then reconsider tt = tt as Subset of T ;
take tt ; :: thesis: for t being type of T holds
( t in tt iff for a being adjective of T st a in A holds
t in types a )
thus for t being type of T holds
( t in tt iff for a being adjective of T st a in A holds
t in types a ) by A1; :: thesis: verum