defpred S₁[ Sequence, Surreal] means ( $2 in union (rng $1) or ( dom $1 = born_eq $2 & ex Y being non empty surreal-membered set st
( Y = (born_eq_set $2) /\ (made_of (union (rng $1))) & $2 = the b₁ -smallest Surreal ) ) );
deffunc H₁( Sequence) -> set = { e where e is Element of Day (dom $1) : for x being Surreal st x = e holds
S₁[$1,x] } ;
consider IT being Sequence such that
A1: dom IT = succ A and
A2: for B being Ordinal
for L1 being Sequence st B in succ A & L1 = IT | B holds
IT . B = H₁(L1) from ORDINAL1:sch 4();
take IT ; :: thesis: ( dom IT = succ A & ( for B being Ordinal st B in succ A holds
( IT . B c= Day B & ( for x being Surreal holds
( x in IT . B iff ( x in union (rng (IT | B)) or ( B = born_eq x & ex Y being non empty surreal-membered set st
( Y = (born_eq_set x) /\ (made_of (union (rng (IT | B)))) & x = the b₃ -smallest Surreal ) ) ) ) ) ) ) )
thus dom IT = succ A by A1; :: thesis: for B being Ordinal st B in succ A holds
( IT . B c= Day B & ( for x being Surreal holds
( x in IT . B iff ( x in union (rng (IT | B)) or ( B = born_eq x & ex Y being non empty surreal-membered set st
( Y = (born_eq_set x) /\ (made_of (union (rng (IT | B)))) & x = the b₃ -smallest Surreal ) ) ) ) ) )
let B be Ordinal; :: thesis: ( B in succ A implies ( IT . B c= Day B & ( for x being Surreal holds
( x in IT . B iff ( x in union (rng (IT | B)) or ( B = born_eq x & ex Y being non empty surreal-membered set st
( Y = (born_eq_set x) /\ (made_of (union (rng (IT | B)))) & x = the b₂ -smallest Surreal ) ) ) ) ) ) )
assume A3: B in succ A ; :: thesis: ( IT . B c= Day B & ( for x being Surreal holds
( x in IT . B iff ( x in union (rng (IT | B)) or ( B = born_eq x & ex Y being non empty surreal-membered set st
( Y = (born_eq_set x) /\ (made_of (union (rng (IT | B)))) & x = the b₂ -smallest Surreal ) ) ) ) ) )
set L1 = IT | B;
A4: dom (IT | B) = B by RELAT_1:62, A1, A3, ORDINAL1:def 2;
thus IT . B c= Day B :: thesis: for x being Surreal holds
( x in IT . B iff ( x in union (rng (IT | B)) or ( B = born_eq x & ex Y being non empty surreal-membered set st
( Y = (born_eq_set x) /\ (made_of (union (rng (IT | B)))) & x = the b₂ -smallest Surreal ) ) ) )

proof

let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in IT . B or o in Day B )
assume o in IT . B ; :: thesis: o in Day B
then o in H₁(IT | B) by A3, A2;
then ex e being Element of Day (dom (IT | B)) st
( o = e & ( for x being Surreal st x = e holds
S₁[IT | B,x] ) ) ;
hence o in Day B by A4; :: thesis: verum

end;

let x be Surreal; :: thesis: ( x in IT . B iff ( x in union (rng (IT | B)) or ( B = born_eq x & ex Y being non empty surreal-membered set st
( Y = (born_eq_set x) /\ (made_of (union (rng (IT | B)))) & x = the b₁ -smallest Surreal ) ) ) )
thus ( not x in IT . B or x in union (rng (IT | B)) or ( B = born_eq x & ex Y being non empty surreal-membered set st
( Y = (born_eq_set x) /\ (made_of (union (rng (IT | B)))) & x = the b₁ -smallest Surreal ) ) ) :: thesis: ( ( x in union (rng (IT | B)) or ( B = born_eq x & ex Y being non empty surreal-membered set st
( Y = (born_eq_set x) /\ (made_of (union (rng (IT | B)))) & x = the b₁ -smallest Surreal ) ) ) implies x in IT . B )

proof

assume A5: ( x in IT . B & not x in union (rng (IT | B)) ) ; :: thesis: ( B = born_eq x & ex Y being non empty surreal-membered set st
( Y = (born_eq_set x) /\ (made_of (union (rng (IT | B)))) & x = the b₁ -smallest Surreal ) )
then x in H₁(IT | B) by A3, A2;
then consider e being Element of Day (dom (IT | B)) such that
A6: ( x = e & ( for y being Surreal st y = e holds
S₁[IT | B,y] ) ) ;
thus ( B = born_eq x & ex Y being non empty surreal-membered set st
( Y = (born_eq_set x) /\ (made_of (union (rng (IT | B)))) & x = the b₁ -smallest Surreal ) ) by A4, A6, A5; :: thesis: verum

end;

assume ( x in union (rng (IT | B)) or ( B = born_eq x & ex Y being non empty surreal-membered set st
( Y = (born_eq_set x) /\ (made_of (union (rng (IT | B)))) & x = the b₁ -smallest Surreal ) ) ) ; :: thesis: x in IT . B

per cases then ( x in union (rng (IT | B)) or ( B = born_eq x & ex Y being non empty surreal-membered set st
( Y = (born_eq_set x) /\ (made_of (union (rng (IT | B)))) & x = the b₁ -smallest Surreal ) ) ) ;

suppose A7: x in union (rng (IT | B)) ; :: thesis: x in IT . B

then consider Y being set such that
A8: ( x in Y & Y in rng (IT | B) ) by TARSKI:def 4;
consider C being object such that
A9: ( C in dom (IT | B) & (IT | B) . C = Y ) by A8, FUNCT_1:def 3;
reconsider C = C as Ordinal by A9;
defpred S₂[ Ordinal] means ( x in IT . $1 & $1 in B );
(IT | B) . C = IT . C by A9, FUNCT_1:47;
then A10: ex C being Ordinal st S₂[C] by A9, A8;
consider D being Ordinal such that
A11: ( S₂[D] & ( for E being Ordinal st S₂[E] holds
D c= E ) ) from ORDINAL1:sch 1(A10);
IT . D = H₁(IT | D) by A2, A11, A3, ORDINAL1:10;
then consider d being Element of Day (dom (IT | D)) such that
A12: ( x = d & ( for y being Surreal st y = d holds
S₁[IT | D,y] ) ) by A11;
D in succ A by A11, A3, ORDINAL1:10;
then A13: dom (IT | D) = D by RELAT_1:62, A1, ORDINAL1:def 2;
A14: x in Day D by A12, A13;
A15: Day D c= Day B by SURREAL0:35, A11, ORDINAL1:def 2;
for y being Surreal st y = x holds
S₁[IT | B,y] by A7;
then x in H₁(IT | B) by A15, A14, A4;
hence x in IT . B by A2, A3; :: thesis: verum

end;

suppose A16: ( B = born_eq x & ex Y being non empty surreal-membered set st
( Y = (born_eq_set x) /\ (made_of (union (rng (IT | B)))) & x = the b₁ -smallest Surreal ) ) ; :: thesis: x in IT . B

consider Y being non empty surreal-membered set such that
A17: ( Y = (born_eq_set x) /\ (made_of (union (rng (IT | B)))) & x = the Y -smallest Surreal ) by A16;
x in Y by A17, Def7;
then x in born_eq_set x by A17, XBOOLE_0:def 4;
then x in Day (born_eq x) by Def6;
then ( born_eq x c= born x & born x c= born_eq x ) by Def5, SURREAL0:def 18;
then A18: born_eq x = born x by XBOOLE_0:def 10;
A19: x in Day (dom (IT | B)) by A4, A16, A18, SURREAL0:def 18;
for y being Surreal st y = x holds
S₁[IT | B,y] by RELAT_1:62, A1, A3, ORDINAL1:def 2, A16;
then x in H₁(IT | B) by A19;
hence x in IT . B by A3, A2; :: thesis: verum

end;

end;