let x, y be Surreal; :: thesis: ( x == y implies born_eq_set x c= born_eq_set y )
assume A1: x == y ; :: thesis: born_eq_set x c= born_eq_set y
let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in born_eq_set x or o in born_eq_set y )
assume A2: o in born_eq_set x ; :: thesis: o in born_eq_set y
then reconsider o = o as Surreal by SURREAL0:def 16;
A3: born_eq x = born_eq y by A1, Th33;
A4: ( o == x & o in Day (born_eq x) ) by A2, Def6;
then o == y by A1, Th4;
hence o in born_eq_set y by A3, A4, Def6; :: thesis: verum