let x, y be Surreal; :: thesis: ( y in born_eq_set x implies ( born y = born_eq y & born_eq y = born_eq x ) )
assume A1: y in born_eq_set x ; :: thesis: ( born y = born_eq y & born_eq y = born_eq x )
then y in Day (born_eq x) by Def6;
then A2: born y c= born_eq x by SURREAL0:def 18;
x == y by A1, Def6;
then A3: born_eq x = born_eq y by Th33;
born_eq y c= born y by Def5;
hence ( born y = born_eq y & born_eq y = born_eq x ) by A2, A3, XBOOLE_0:def 10; :: thesis: verum