defpred S₁[ object ] means for y being Surreal st y = $1 holds
0_No < y;
consider P being set such that
A1: for o being object holds
( o in P iff ( o in Day A & S₁[o] ) ) from XBOOLE_0:sch 1();
P c= Day A

proof

let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in P or o in Day A )
thus ( not o in P or o in Day A ) by A1; :: thesis: verum

end;

then reconsider P = P as Subset of (Day A) ;
take P ; :: thesis: for x being Surreal holds
( x in P iff ( x in Day A & 0_No < x ) )
let x be Surreal; :: thesis: ( x in P iff ( x in Day A & 0_No < x ) )
thus ( x in P implies ( x in Day A & 0_No < x ) ) by A1; :: thesis: ( x in Day A & 0_No < x implies x in P )
assume A2: ( x in Day A & 0_No < x ) ; :: thesis: x in P
then S₁[x] ;
hence x in P by A2, A1; :: thesis: verum