defpred S₁[ object ] 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 object holds
( x in tt iff ( x in the carrier of T & S₁[x] ) ) from XBOOLE_0:sch 1();
tt c= the carrier of T by A1;
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