let x be Surreal; :: thesis: - (- x) = x
x in Day (born x) by SURREAL0:def 18;
hence - (- x) = x by Lm1; :: thesis: verum