let x, y be Surreal; :: thesis: ( x == y implies born_eq_set x = born_eq_set y )
assume x == y ; :: thesis: born_eq_set x = born_eq_set y
then ( born_eq_set x c= born_eq_set y & born_eq_set y c= born_eq_set x ) by Lm1;
hence born_eq_set x = born_eq_set y by XBOOLE_0:def 10; :: thesis: verum