let P1, P2 be Subset of (Day A); :: thesis: ( ( for x being Surreal holds
( x in P1 iff ( x in Day A & 0_No < x ) ) ) & ( for x being Surreal holds
( x in P2 iff ( x in Day A & 0_No < x ) ) ) implies P1 = P2 )
assume that
A3: for x being Surreal holds
( x in P1 iff ( x in Day A & 0_No < x ) ) and
A4: for x being Surreal holds
( x in P2 iff ( x in Day A & 0_No < x ) ) ; :: thesis: P1 = P2
for o being object st o in P1 holds
o in P2

proof

let o be object ; :: thesis: ( o in P1 implies o in P2 )
assume A5: o in P1 ; :: thesis: o in P2
then reconsider x = o as Surreal ;
( x in Day A & 0_No < x ) by A3, A5;
hence o in P2 by A4; :: thesis: verum

end;

then A6: P1 c= P2 by TARSKI:def 3;
for o being object st o in P2 holds
o in P1

proof

let o be object ; :: thesis: ( o in P2 implies o in P1 )
assume A7: o in P2 ; :: thesis: o in P1
then reconsider x = o as Surreal ;
( x in Day A & 0_No < x ) by A4, A7;
hence o in P1 by A3; :: thesis: verum

end;

then P2 c= P1 by TARSKI:def 3;
hence P1 = P2 by A6, XBOOLE_0:def 10; :: thesis: verum