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