let x be Surreal; :: thesis: ( ( x is uSurreal & born x is finite ) iff ex d being Dyadic st x = uDyadic . d )

hereby :: thesis: ( ex d being Dyadic st x = uDyadic . d implies ( x is uSurreal & born x is finite ) )

assume A1: ( x is uSurreal & born x is finite ) ; :: thesis: ex d being Dyadic st x = uDyadic . d
then reconsider b = born x as Nat ;
x in Day b by SURREAL0:def 18;
then ex d being Dyadic st
( x == uDyadic . d & uDyadic . d in Day b ) by Th35;
hence ex d being Dyadic st x = uDyadic . d by A1, SURREALO:50; :: thesis: verum

end;

given d being Dyadic such that A2: x = uDyadic . d ; :: thesis: ( x is uSurreal & born x is finite )
consider n being Nat such that
A3: uDyadic . d in Day n by Th36;
born (uDyadic . d) c= n by A3, SURREAL0:def 18;
hence ( x is uSurreal & born x is finite ) by A2; :: thesis: verum