theorem Th23: :: SURREALO:23

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