let x, y be Surreal; :: thesis: ( x == y implies born_eq x = born_eq y )
assume A1: x == y ; :: thesis: born_eq x = born_eq y
consider z being Surreal such that
A2: ( born z = born_eq x & z == x ) by Def5;
z == y by A1, A2, Th4;
then A3: born_eq y c= born_eq x by A2, Def5;
consider t being Surreal such that
A4: ( born t = born_eq y & t == y ) by Def5;
t == x by A1, A4, Th4;
then born_eq x c= born_eq y by A4, Def5;
hence born_eq x = born_eq y by A3, XBOOLE_0:def 10; :: thesis: verum