theorem Th24: :: SURREALO:24

for x, Min being Surreal st ( for y being Surreal st y in R_ x holds
Min <= y ) & Min in R_ x holds
( [(L_ x),{Min}] is Surreal & ( for y being Surreal st y = [(L_ x),{Min}] holds
( y == x & born y c= born x ) ) )