defpred S₁[ object ] means ex t being type of T st
( $1 = t & a in adjs t );
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 x being object holds
( x in tt iff ex t being type of T st
( x = t & a in adjs t ) )
let x be object ; :: 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 :: thesis: x in the carrier of T

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