let x be Surreal; :: thesis: L_ x << R_ x
let l, r be Surreal; :: according to SURREAL0:def 20 :: thesis: ( l in L_ x & r in R_ x implies not r <= l )
assume A1: ( l in L_ x & r in R_ x ) ; :: thesis: not r <= l
consider A being Ordinal such that
A2: x in Day A by Def14;
set S = No_Ord A;
A3: L_ x << No_Ord A, R_ x by A2, Th7;
l in (L_ x) \/ (R_ x) by A1, XBOOLE_0:def 3;
then consider OL being Ordinal such that
A4: ( OL in A & l in Day ((No_Ord A),OL) ) by A2, Th7;
OL c= A by A4, ORDINAL1:def 2;
then A5: ( l in Day OL & Day OL c= Day A ) by A4, Th35, Th36;
r in (L_ x) \/ (R_ x) by A1, XBOOLE_0:def 3;
then consider OR being Ordinal such that
A6: ( OR in A & r in Day ((No_Ord A),OR) ) by A2, Th7;
OR c= A by A6, ORDINAL1:def 2;
then ( r in Day OR & Day OR c= Day A ) by A6, Th35, Th36;
hence not r <= l by A3, A1, A5, Th40; :: thesis: verum