let A be Ordinal; :: thesis: for x being Surreal st x in Day A holds
x <= No_uOrdinal_op A
let x be Surreal; :: thesis: ( x in Day A implies x <= No_uOrdinal_op A )
assume x in Day A ; :: thesis: x <= No_uOrdinal_op A
then ( x <= No_Ordinal_op A & No_Ordinal_op A == No_uOrdinal_op A ) by Th69, Th73;
hence x <= No_uOrdinal_op A by SURREALO:4; :: thesis: verum