defpred S₁[ object ] means for y being Element of E st y = $1 holds
x,y are_conjugated_under T;
set Y = { y where y is Element of E : x,y are_conjugated_under T } ;
consider X being Subset of E such that
A1: for y being Element of E holds
( y in X iff S₁[y] ) from SUBSET_1:sch 3();

now :: thesis: for y being object holds
( ( y in X implies y in { y where y is Element of E : x,y are_conjugated_under T } ) & ( y in { y where y is Element of E : x,y are_conjugated_under T } implies y in X ) )

let y be object ; :: thesis: ( ( y in X implies y in { y where y is Element of E : x,y are_conjugated_under T } ) & ( y in { y where y is Element of E : x,y are_conjugated_under T } implies y in X ) )

hereby :: thesis: ( y in { y where y is Element of E : x,y are_conjugated_under T } implies y in X )

assume A2: y in X ; :: thesis: y in { y where y is Element of E : x,y are_conjugated_under T }
then reconsider y9 = y as Element of E ;
x,y9 are_conjugated_under T by A1, A2;
hence y in { y where y is Element of E : x,y are_conjugated_under T } ; :: thesis: verum

end;

assume y in { y where y is Element of E : x,y are_conjugated_under T } ; :: thesis: y in X
then A3: ex y9 being Element of E st
( y9 = y & x,y9 are_conjugated_under T ) ;
then S₁[y] ;
hence y in X by A1, A3; :: thesis: verum

end;

hence { y where y is Element of E : x,y are_conjugated_under T } is Subset of E by TARSKI:2; :: thesis: verum