let x be Surreal; :: thesis: born (NonNegativePart x) c= born x
set NN = NonNegativePart x;
for o being object st o in (L_ (NonNegativePart x)) \/ (R_ (NonNegativePart x)) holds
ex O being Ordinal st
( O in born x & o in Day O )

proof

let o be object ; :: thesis: ( o in (L_ (NonNegativePart x)) \/ (R_ (NonNegativePart x)) implies ex O being Ordinal st
( O in born x & o in Day O ) )
assume A1: o in (L_ (NonNegativePart x)) \/ (R_ (NonNegativePart x)) ; :: thesis: ex O being Ordinal st
( O in born x & o in Day O )
reconsider o = o as Surreal by A1, SURREAL0:def 16;
( ( o in L_ (NonNegativePart x) & L_ (NonNegativePart x) c= L_ x ) or ( o in R_ (NonNegativePart x) & R_ (NonNegativePart x) c= R_ x ) ) by A1, Th1, XBOOLE_0:def 3;
then o in (L_ x) \/ (R_ x) by XBOOLE_0:def 3;
then ( born o in born x & o in Day (born o) ) by SURREALO:1, SURREAL0:def 18;
hence ex O being Ordinal st
( O in born x & o in Day O ) ; :: thesis: verum

end;

then [(L_ (NonNegativePart x)),(R_ (NonNegativePart x))] in Day (born x) by SURREAL0:45, SURREAL0:46;
hence born (NonNegativePart x) c= born x by SURREAL0:def 18; :: thesis: verum