set B = born_eq x;
set M = unique_No_op (born_eq x);
let s1, s2 be Surreal; :: thesis: ( s1 == x & s1 in (unique_No_op (born_eq x)) . (born_eq x) & s2 == x & s2 in (unique_No_op (born_eq x)) . (born_eq x) implies s1 = s2 )
assume that
A43: ( s1 == x & s1 in (unique_No_op (born_eq x)) . (born_eq x) ) and
A44: ( s2 == x & s2 in (unique_No_op (born_eq x)) . (born_eq x) ) ; :: thesis: s1 = s2
( born s1 = born_eq s1 & born_eq s1 = born_eq x & born_eq x = born_eq s2 & born_eq s2 = born s2 ) by A43, A44, Th33, Th38;
then A45: ( not s1 in union (rng ((unique_No_op (born_eq x)) | (born_eq x))) & not s2 in union (rng ((unique_No_op (born_eq x)) | (born_eq x))) ) by A43, A44, Th38;
A46: born_eq x in succ (born_eq x) by ORDINAL1:6;
consider Y1 being non empty surreal-membered set such that
A47: ( Y1 = (born_eq_set s1) /\ (made_of (union (rng ((unique_No_op (born_eq x)) | (born_eq x))))) & s1 = the Y1 -smallest Surreal ) by A43, A45, A46, Def9;
consider Y2 being non empty surreal-membered set such that
A48: ( Y2 = (born_eq_set s2) /\ (made_of (union (rng ((unique_No_op (born_eq x)) | (born_eq x))))) & s2 = the Y2 -smallest Surreal ) by A44, A45, A46, Def9;
s1 == s2 by A43, A44, Th4;
then Y1 = Y2 by A47, A48, Th34;
hence s1 = s2 by A47, A48; :: thesis: verum