let x, y be Surreal; :: thesis: ( y in (L_ x) \/ (R_ x) implies born y in born x )
assume A1: y in (L_ x) \/ (R_ x) ; :: thesis: born y in born x
A2: x = [(L_ x),(R_ x)] ;
x in Day (born x) by SURREAL0:def 18;
then consider O being Ordinal such that
A3: ( O in born x & y in Day O ) by SURREAL0:46, A1, A2;
born y c= O by A3, SURREAL0:def 18;
hence born y in born x by A3, ORDINAL1:12; :: thesis: verum