set NN = NonNegativePart x;
let s1, s2 be pair set ; :: thesis: ( ( for o being object holds
( ( o in L_ s1 implies ex l being Surreal st
( o = sqrt l & l in L_ (NonNegativePart x) ) ) & ( ex l being Surreal st
( o = sqrt l & l in L_ (NonNegativePart x) ) implies o in L_ s1 ) & ( o in R_ s1 implies ex r being Surreal st
( o = sqrt r & r in R_ (NonNegativePart x) ) ) & ( ex r being Surreal st
( o = sqrt r & r in R_ (NonNegativePart x) ) implies o in R_ s1 ) ) ) & ( for o being object holds
( ( o in L_ s2 implies ex l being Surreal st
( o = sqrt l & l in L_ (NonNegativePart x) ) ) & ( ex l being Surreal st
( o = sqrt l & l in L_ (NonNegativePart x) ) implies o in L_ s2 ) & ( o in R_ s2 implies ex r being Surreal st
( o = sqrt r & r in R_ (NonNegativePart x) ) ) & ( ex r being Surreal st
( o = sqrt r & r in R_ (NonNegativePart x) ) implies o in R_ s2 ) ) ) implies s1 = s2 )
assume that
A3: for o being object holds
( ( o in L_ s1 implies ex l being Surreal st
( o = sqrt l & l in L_ (NonNegativePart x) ) ) & ( ex l being Surreal st
( o = sqrt l & l in L_ (NonNegativePart x) ) implies o in L_ s1 ) & ( o in R_ s1 implies ex r being Surreal st
( o = sqrt r & r in R_ (NonNegativePart x) ) ) & ( ex r being Surreal st
( o = sqrt r & r in R_ (NonNegativePart x) ) implies o in R_ s1 ) ) and
A4: for o being object holds
( ( o in L_ s2 implies ex l being Surreal st
( o = sqrt l & l in L_ (NonNegativePart x) ) ) & ( ex l being Surreal st
( o = sqrt l & l in L_ (NonNegativePart x) ) implies o in L_ s2 ) & ( o in R_ s2 implies ex r being Surreal st
( o = sqrt r & r in R_ (NonNegativePart x) ) ) & ( ex r being Surreal st
( o = sqrt r & r in R_ (NonNegativePart x) ) 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 = sqrt r & r in R_ (NonNegativePart x) ) ) by A3;
hence ( o in R_ s1 iff o in R_ s2 ) by A4; :: thesis: verum

end;

then A5: 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 = sqrt l & l in L_ (NonNegativePart x) ) ) by A3;
hence ( o in L_ s1 iff o in L_ s2 ) by A4; :: thesis: verum

end;

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