let x, y be Surreal; :: thesis: born (x + y) c= (born x) (+) (born y)
x + y in Day ((born x) (+) (born y)) by Lm5;
hence born (x + y) c= (born x) (+) (born y) by SURREAL0:def 18; :: thesis: verum