let r be Real; :: thesis: born (sReal . r) c= omega
sReal . r in Day omega by Lm10;
hence born (sReal . r) c= omega by SURREAL0:def 18; :: thesis: verum