consider A being Ordinal such that
A5: x in Day A by Def14;
let S be set ; :: thesis: ( S = R_ x implies S is surreal-membered )
assume A6: S = R_ x ; :: thesis: S is surreal-membered
let y be object ; :: according to SURREAL0:def 16 :: thesis: ( y in S implies y is surreal )
assume A7: y in S ; :: thesis: y is surreal
y in (L_ x) \/ (R_ x) by A6, A7, XBOOLE_0:def 3;
then consider O being Ordinal such that
A8: ( O in A & y in Day ((No_Ord A),O) ) by A5, Th7;
( Day ((No_Ord A),O) c= Day ((No_Ord A),A) & Day ((No_Ord A),A) = Day A ) by Th9, A8, ORDINAL1:def 2;
hence y is surreal by A8; :: thesis: verum