theorem :: SURREALR:11

for x being Surreal
for D being Ordinal st x in Day D holds
- x in Day D by Lm1;