defpred S₁[ set ] means ex t being type of T st
( $1 = t & a in adjs t );
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 x being set holds
( x in tt iff ex t being type of T st
( x = t & a in adjs t ) )
let x be set ; :: thesis: ( x in tt iff ex t being type of T st
( x = t & a in adjs t ) )
thus ( x in tt implies ex t being type of T st
( x = t & a in adjs t ) ) by A1; :: thesis: ( ex t being type of T st
( x = t & a in adjs t ) implies x in tt )
given t being type of T such that A2: x = t and
A3: a in adjs t ; :: thesis: x in tt

now

A4: dom the adj-map of T = the carrier of T by FUNCT_2:def 1;
assume not x in the carrier of T ; :: thesis: contradiction
hence contradiction by A2, A3, A4, FUNCT_1:def 2; :: thesis: verum

end;

hence x in tt by A1, A2, A3; :: thesis: verum