let s1, s2 be positive Surreal; :: thesis: ( ( for y being Surreal holds
( ( not y in L_ s1 or y = 0_No or ( y in L_ x & y is positive ) ) & ( ( y = 0_No or ( y in L_ x & y is positive ) ) implies y in L_ s1 ) & ( y in R_ s1 implies ( y in R_ x & y is positive ) ) & ( y in R_ x & y is positive implies y in R_ s1 ) ) ) & ( for y being Surreal holds
( ( not y in L_ s2 or y = 0_No or ( y in L_ x & y is positive ) ) & ( ( y = 0_No or ( y in L_ x & y is positive ) ) implies y in L_ s2 ) & ( y in R_ s2 implies ( y in R_ x & y is positive ) ) & ( y in R_ x & y is positive implies y in R_ s2 ) ) ) implies s1 = s2 )
assume that
A5: for y being Surreal holds
( ( not y in L_ s1 or y = 0_No or ( y in L_ x & y is positive ) ) & ( ( y = 0_No or ( y in L_ x & y is positive ) ) implies y in L_ s1 ) & ( y in R_ s1 implies ( y in R_ x & y is positive ) ) & ( y in R_ x & y is positive implies y in R_ s1 ) ) and
A6: for y being Surreal holds
( ( not y in L_ s2 or y = 0_No or ( y in L_ x & y is positive ) ) & ( ( y = 0_No or ( y in L_ x & y is positive ) ) implies y in L_ s2 ) & ( y in R_ s2 implies ( y in R_ x & y is positive ) ) & ( y in R_ x & y is positive implies y in R_ s2 ) ) ; :: thesis: s1 = s2
for o being object st o in L_ s1 holds
o in L_ s2

proof

let o be object ; :: thesis: ( o in L_ s1 implies o in L_ s2 )
assume A7: o in L_ s1 ; :: thesis: o in L_ s2
then reconsider o = o as Surreal by SURREAL0:def 16;
( o = 0_No or ( o in L_ x & o is positive ) ) by A7, A5;
hence o in L_ s2 by A6; :: thesis: verum

end;

then A8: L_ s1 c= L_ s2 by TARSKI:def 3;
for o being object st o in L_ s2 holds
o in L_ s1

proof

let o be object ; :: thesis: ( o in L_ s2 implies o in L_ s1 )
assume A9: o in L_ s2 ; :: thesis: o in L_ s1
then reconsider o = o as Surreal by SURREAL0:def 16;
( o = 0_No or ( o in L_ x & o is positive ) ) by A9, A6;
hence o in L_ s1 by A5; :: thesis: verum

end;

then L_ s2 c= L_ s1 by TARSKI:def 3;
then A10: L_ s1 = L_ s2 by A8, XBOOLE_0:def 10;
for o being object st o in R_ s1 holds
o in R_ s2

proof

let o be object ; :: thesis: ( o in R_ s1 implies o in R_ s2 )
assume A11: o in R_ s1 ; :: thesis: o in R_ s2
then reconsider o = o as Surreal by SURREAL0:def 16;
( o in R_ x & o is positive ) by A11, A5;
hence o in R_ s2 by A6; :: thesis: verum

end;

then A12: R_ s1 c= R_ s2 by TARSKI:def 3;
for o being object st o in R_ s2 holds
o in R_ s1

proof

let o be object ; :: thesis: ( o in R_ s2 implies o in R_ s1 )
assume A13: o in R_ s2 ; :: thesis: o in R_ s1
then reconsider o = o as Surreal by SURREAL0:def 16;
( o in R_ x & o is positive ) by A13, A6;
hence o in R_ s1 by A5; :: thesis: verum

end;

then R_ s2 c= R_ s1 by TARSKI:def 3;
then R_ s1 = R_ s2 by A12, XBOOLE_0:def 10;
hence s1 = s2 by A10, XTUPLE_0:2; :: thesis: verum