set NN = NonNegativePart x;
set L = { (sqrt l) where l is Element of L_ (NonNegativePart x) : l in L_ (NonNegativePart x) } ;
set R = { (sqrt r) where r is Element of R_ (NonNegativePart x) : r in R_ (NonNegativePart x) } ;
reconsider IT = [ { (sqrt l) where l is Element of L_ (NonNegativePart x) : l in L_ (NonNegativePart x) } , { (sqrt r) where r is Element of R_ (NonNegativePart x) : r in R_ (NonNegativePart x) } ] as pair set by TARSKI:1;
take IT ; :: thesis:
let o be object ; :: thesis:
thus ( o in L_ IT implies ex l being Surreal st
( o = sqrt l & l in L_ (NonNegativePart x) ) ) :: thesis:

proof

assume o in L_ IT ; :: thesis:
then consider l being Element of L_ (NonNegativePart x) such that
A1: ( o = sqrt l & l in L_ (NonNegativePart x) ) ;
reconsider l = l as Surreal by A1, SURREAL0:def 16;
take l ; :: thesis:
thus ( o = sqrt l & l in L_ (NonNegativePart x) ) by A1; :: thesis:

end;

thus ( ex l being Surreal st
( o = sqrt l & l in L_ (NonNegativePart x) ) implies o in L_ IT ) ; :: thesis:
thus ( o in R_ IT implies ex r being Surreal st
( o = sqrt r & r in R_ (NonNegativePart x) ) ) :: thesis:

proof

assume o in R_ IT ; :: thesis:
then consider r being Element of R_ (NonNegativePart x) such that
A2: ( o = sqrt r & r in R_ (NonNegativePart x) ) ;
reconsider r = r as Surreal by A2, SURREAL0:def 16;
take r ; :: thesis:
thus ( o = sqrt r & r in R_ (NonNegativePart x) ) by A2; :: thesis:

end;

thus ( ex r being Surreal st
( o = sqrt r & r in R_ (NonNegativePart x) ) implies o in R_ IT ) ; :: thesis: