let x be Surreal; :: thesis: ( x is positive implies born ||.x.|| c= born x )
A1: 0_No <= 0_No ;
assume A2: x is positive ; :: thesis: born ||.x.|| c= born x
then A3: {} in born x by A1, SURREAL0:37, ORDINAL3:8;
A4: born 0_No = {} by SURREAL0:37;
set Nx = ||.x.||;
for o being object st o in (L_ ||.x.||) \/ (R_ ||.x.||) holds
ex O being Ordinal st
( O in born x & o in Day O )

proof

let o be object ; :: thesis: ( o in (L_ ||.x.||) \/ (R_ ||.x.||) implies ex O being Ordinal st
( O in born x & o in Day O ) )
assume A5: o in (L_ ||.x.||) \/ (R_ ||.x.||) ; :: thesis: ex O being Ordinal st
( O in born x & o in Day O )
then reconsider o = o as Surreal by SURREAL0:def 16;

per cases ( o = 0_No or o <> 0_No ) ;

suppose o = 0_No ; :: thesis: ex O being Ordinal st
( O in born x & o in Day O )

then o in Day {} by SURREAL0:def 18, A4;
hence ex O being Ordinal st
( O in born x & o in Day O ) by A3; :: thesis: verum

end;

suppose o <> 0_No ; :: thesis: ex O being Ordinal st
( O in born x & o in Day O )

then A6: o in ((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} by A5, ZFMISC_1:56;
((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} c= (L_ x) \/ (R_ x) by A2, Th20;
then ( born o in born x & o in Day (born o) ) by A6, SURREALO:1, SURREAL0:def 18;
hence ex O being Ordinal st
( O in born x & o in Day O ) ; :: thesis: verum

end;

end;

end;

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