let x, y be Surreal; :: thesis: ( x in born_eq_set y implies - x in born_eq_set (- y) )
assume A1: x in born_eq_set y ; :: thesis: - x in born_eq_set (- y)
then x == y by SURREALO:def 6;
then A2: - x == - y by Th10;
x in Day (born_eq y) by A1, SURREALO:def 6;
then ( born (- x) = born x & born x c= born_eq y & born_eq y = born_eq (- y) ) by SURREAL0:def 18, Th13, Th12;
then ( - x in Day (born (- x)) & Day (born (- x)) c= Day (born_eq (- y)) ) by SURREAL0:def 18, SURREAL0:35;
hence - x in born_eq_set (- y) by A2, SURREALO:def 6; :: thesis: verum