let s1, s2 be pair set ; :: thesis: ( ( for o being object holds
( ( o in L_ s1 implies ex l being Surreal st
( o = l & l in L_ x & 0_No <= l ) ) & ( ex l being Surreal st
( o = l & l in L_ x & 0_No <= l ) implies o in L_ s1 ) & ( o in R_ s1 implies ex r being Surreal st
( o = r & r in R_ x & 0_No <= r ) ) & ( ex r being Surreal st
( o = r & r in R_ x & 0_No <= r ) implies o in R_ s1 ) ) ) & ( for o being object holds
( ( o in L_ s2 implies ex l being Surreal st
( o = l & l in L_ x & 0_No <= l ) ) & ( ex l being Surreal st
( o = l & l in L_ x & 0_No <= l ) implies o in L_ s2 ) & ( o in R_ s2 implies ex r being Surreal st
( o = r & r in R_ x & 0_No <= r ) ) & ( ex r being Surreal st
( o = r & r in R_ x & 0_No <= r ) implies o in R_ s2 ) ) ) implies s1 = s2 )
assume that
A5: for o being object holds
( ( o in L_ s1 implies ex l being Surreal st
( o = l & l in L_ x & 0_No <= l ) ) & ( ex l being Surreal st
( o = l & l in L_ x & 0_No <= l ) implies o in L_ s1 ) & ( o in R_ s1 implies ex r being Surreal st
( o = r & r in R_ x & 0_No <= r ) ) & ( ex r being Surreal st
( o = r & r in R_ x & 0_No <= r ) implies o in R_ s1 ) ) and
A6: for o being object holds
( ( o in L_ s2 implies ex l being Surreal st
( o = l & l in L_ x & 0_No <= l ) ) & ( ex l being Surreal st
( o = l & l in L_ x & 0_No <= l ) implies o in L_ s2 ) & ( o in R_ s2 implies ex r being Surreal st
( o = r & r in R_ x & 0_No <= r ) ) & ( ex r being Surreal st
( o = r & r in R_ x & 0_No <= r ) implies o in R_ s2 ) ) ; :: thesis: s1 = s2

now :: thesis: for o being object holds
( o in R_ s1 iff o in R_ s2 )

let o be object ; :: thesis: ( o in R_ s1 iff o in R_ s2 )
( o in R_ s1 iff ex r being Surreal st
( o = r & r in R_ x & 0_No <= r ) ) by A5;
hence ( o in R_ s1 iff o in R_ s2 ) by A6; :: thesis: verum

end;

then A7: R_ s1 = R_ s2 by TARSKI:2;

now :: thesis: for o being object holds
( o in L_ s1 iff o in L_ s2 )

let o be object ; :: thesis: ( o in L_ s1 iff o in L_ s2 )
( o in L_ s1 iff ex l being Surreal st
( o = l & l in L_ x & 0_No <= l ) ) by A5;
hence ( o in L_ s1 iff o in L_ s2 ) by A6; :: thesis: verum

end;

then L_ s1 = L_ s2 by TARSKI:2;
hence s1 = s2 by A7, XTUPLE_0:2; :: thesis: verum