let x be Surreal; :: thesis: ( born x is finite implies ( L_ x is finite & R_ x is finite ) )
assume born x is finite ; :: thesis: ( L_ x is finite & R_ x is finite )
then A1: Day (born x) is finite by Th7;
A2: (L_ x) \/ (R_ x) c= Day (born x)

proof

let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in (L_ x) \/ (R_ x) or o in Day (born x) )
assume A3: o in (L_ x) \/ (R_ x) ; :: thesis: o in Day (born x)
then reconsider y = o as Surreal by SURREAL0:def 16;
born y in born x by A3, Th1;
then ( y in Day (born y) & Day (born y) c= Day (born x) ) by SURREAL0:35, SURREAL0:def 18, ORDINAL1:def 2;
hence o in Day (born x) ; :: thesis: verum

end;

( L_ x c= (L_ x) \/ (R_ x) & R_ x c= (L_ x) \/ (R_ x) ) by XBOOLE_1:7;
hence ( L_ x is finite & R_ x is finite ) by A2, A1; :: thesis: verum