let A, B be Ordinal; :: thesis: for x being Surreal st x in (unique_No_op A) . B holds
( born_eq x = born x & born x c= B & x in (unique_No_op A) . (born x) & not x in union (rng ((unique_No_op A) | (born x))) )
let x be Surreal; :: thesis: ( x in (unique_No_op A) . B implies ( born_eq x = born x & born x c= B & x in (unique_No_op A) . (born x) & not x in union (rng ((unique_No_op A) | (born x))) ) )
set M = unique_No_op A;
assume A1: x in (unique_No_op A) . B ; :: thesis: ( born_eq x = born x & born x c= B & x in (unique_No_op A) . (born x) & not x in union (rng ((unique_No_op A) | (born x))) )
then B in dom (unique_No_op A) by FUNCT_1:def 2;
then A2: B in succ A by Def9;
defpred S₁[ Ordinal] means ( x in (unique_No_op A) . $1 & $1 in succ A );
A3: ex C being Ordinal st S₁[C] by A1, A2;
consider D being Ordinal such that
A4: ( S₁[D] & ( for E being Ordinal st S₁[E] holds
D c= E ) ) from ORDINAL1:sch 1(A3);
A5: not x in union (rng ((unique_No_op A) | D))

proof

assume x in union (rng ((unique_No_op A) | D)) ; :: thesis: contradiction
then consider Z being set such that
A6: ( x in Z & Z in rng ((unique_No_op A) | D) ) by TARSKI:def 4;
consider E being object such that
A7: ( E in dom ((unique_No_op A) | D) & ((unique_No_op A) | D) . E = Z ) by A6, FUNCT_1:def 3;
reconsider E = E as Ordinal by A7;
S₁[E] by A4, A7, FUNCT_1:47, A6, ORDINAL1:10;
hence contradiction by A4, A7, ORDINAL1:5; :: thesis: verum

end;

then A8: D = born_eq x by A4, Def9;
consider Y being non empty surreal-membered set such that
A9: ( Y = (born_eq_set x) /\ (made_of (union (rng ((unique_No_op A) | D)))) & x = the Y -smallest Surreal ) by A5, A4, Def9;
x in (born_eq_set x) /\ (made_of (union (rng ((unique_No_op A) | D)))) by A9, Def7;
then x in born_eq_set x by XBOOLE_0:def 4;
then x in Day (born_eq x) by Def6;
then ( born x c= born_eq x & born_eq x c= born x ) by Def5, SURREAL0:def 18;
then born x = born_eq x by XBOOLE_0:def 10;
hence ( born_eq x = born x & born x c= B & x in (unique_No_op A) . (born x) & not x in union (rng ((unique_No_op A) | (born x))) ) by A1, A2, A4, A5, A8; :: thesis: verum