theorem Th36: :: SURREAL0:36
for A, B being Ordinal
for o being object st o in Day ((No_Ord A),B) & B c= A holds
o in Day B