defpred S₁[ object ] means for y being Surreal st y = $1 holds
x == y;
consider X being set such that
A1: for o being object holds
( o in X iff ( o in Day (born_eq x) & S₁[o] ) ) from XBOOLE_0:sch 1();
X is surreal-membered

proof

let o be object ; :: according to SURREAL0:def 16 :: thesis: ( not o in X or o is surreal )
thus ( not o in X or o is surreal ) by A1; :: thesis: verum

end;

then reconsider X = X as surreal-membered set ;
take X ; :: thesis: for y being Surreal holds
( y in X iff ( y == x & y in Day (born_eq x) ) )
let y be Surreal; :: thesis: ( y in X iff ( y == x & y in Day (born_eq x) ) )
thus ( y in X implies ( y == x & y in Day (born_eq x) ) ) by A1; :: thesis: ( y == x & y in Day (born_eq x) implies y in X )
assume A2: ( y == x & y in Day (born_eq x) ) ; :: thesis: y in X
then S₁[y] ;
hence y in X by A1, A2; :: thesis: verum