let A, B be Ordinal; :: thesis: ex R being Relation st
( R preserves_No_Comparison_on ClosedProd (R,A,B) & R c= ClosedProd (R,A,B) )
defpred S₁[ Ordinal] means for B being Ordinal ex R being Relation st
( R preserves_No_Comparison_on ClosedProd (R,$1,B) & R c= ClosedProd (R,$1,B) );
A1: for D being Ordinal st ( for C being Ordinal st C in D holds
S₁[C] ) holds
S₁[D]

proof

let D be Ordinal; :: thesis: ( ( for C being Ordinal st C in D holds
S₁[C] ) implies S₁[D] )
assume A2: for C being Ordinal st C in D holds
S₁[C] ; :: thesis: S₁[D]
let B be Ordinal; :: thesis: ex R being Relation st
( R preserves_No_Comparison_on ClosedProd (R,D,B) & R c= ClosedProd (R,D,B) )
defpred S₂[ object , object ] means for B being Ordinal st B = $1 holds
ex R being Relation st
( $2 = R & R preserves_No_Comparison_on ClosedProd (R,B,B) & R c= ClosedProd (R,B,B) );
A3: for e being object st e in D holds
ex u being object st S₂[e,u]

proof

let e be object ; :: thesis: ( e in D implies ex u being object st S₂[e,u] )
assume A4: e in D ; :: thesis: ex u being object st S₂[e,u]
reconsider E = e as Ordinal by A4;
consider R being Relation such that
A5: ( R preserves_No_Comparison_on ClosedProd (R,E,E) & R c= ClosedProd (R,E,E) ) by A4, A2;
take R ; :: thesis: S₂[e,R]
thus S₂[e,R] by A5; :: thesis: verum

end;

consider Lr being Function such that
A6: ( dom Lr = D & ( for e being object st e in D holds
S₂[e,Lr . e] ) ) from CLASSES1:sch 1(A3);
reconsider Lr = Lr as Sequence by A6, ORDINAL1:def 7;
defpred S₃[ object , object ] means for B being Ordinal
for R being Relation st B = $1 & R = Lr . B holds
$2 = ClosedProd (R,B,B);
A7: for e being object st e in D holds
ex u being object st S₃[e,u]

proof

let e be object ; :: thesis: ( e in D implies ex u being object st S₃[e,u] )
assume A8: e in D ; :: thesis: ex u being object st S₃[e,u]
reconsider E = e as Ordinal by A8;
consider R being Relation such that
A9: ( Lr . E = R & R preserves_No_Comparison_on ClosedProd (R,E,E) & R c= ClosedProd (R,E,E) ) by A8, A6;
take ClosedProd (R,E,E) ; :: thesis: S₃[e, ClosedProd (R,E,E)]
thus S₃[e, ClosedProd (R,E,E)] by A9; :: thesis: verum

end;

consider Lp being Function such that
A10: ( dom Lp = D & ( for e being object st e in D holds
S₃[e,Lp . e] ) ) from CLASSES1:sch 1(A7);
reconsider Lp = Lp as Sequence by A10, ORDINAL1:def 7;
A11: for E being Ordinal st E in dom Lp holds
( ex a, b being Ordinal ex R being Relation st
( R = Lr . E & Lp . E = ClosedProd (R,a,b) ) & Lr . E is Relation & ( for R being Relation st R = Lr . E holds
( R preserves_No_Comparison_on Lp . E & R c= Lp . E ) ) )

proof

let E be Ordinal; :: thesis: ( E in dom Lp implies ( ex a, b being Ordinal ex R being Relation st
( R = Lr . E & Lp . E = ClosedProd (R,a,b) ) & Lr . E is Relation & ( for R being Relation st R = Lr . E holds
( R preserves_No_Comparison_on Lp . E & R c= Lp . E ) ) ) )
assume A12: E in dom Lp ; :: thesis: ( ex a, b being Ordinal ex R being Relation st
( R = Lr . E & Lp . E = ClosedProd (R,a,b) ) & Lr . E is Relation & ( for R being Relation st R = Lr . E holds
( R preserves_No_Comparison_on Lp . E & R c= Lp . E ) ) )
consider R being Relation such that
A13: ( Lr . E = R & R preserves_No_Comparison_on ClosedProd (R,E,E) & R c= ClosedProd (R,E,E) ) by A12, A6, A10;
thus ( ex a, b being Ordinal ex R being Relation st
( R = Lr . E & Lp . E = ClosedProd (R,a,b) ) & Lr . E is Relation & ( for R being Relation st R = Lr . E holds
( R preserves_No_Comparison_on Lp . E & R c= Lp . E ) ) ) by A13, A12, A10; :: thesis: verum

end;

then reconsider RR = union (rng Lr) as Relation by A10, A6, Th24;
A14: ( RR preserves_No_Comparison_on union (rng Lp) & RR c= union (rng Lp) ) by A11, A10, A6, Th24;
A15: union (rng Lp) c= OpenProd (RR,D,{})

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union (rng Lp) or x in OpenProd (RR,D,{}) )
assume x in union (rng Lp) ; :: thesis: x in OpenProd (RR,D,{})
then consider Y being set such that
A16: ( x in Y & Y in rng Lp ) by TARSKI:def 4;
consider E being object such that
A17: ( E in dom Lp & Y = Lp . E ) by A16, FUNCT_1:def 3;
reconsider E = E as Ordinal by A17;
A18: Day (RR,E) c= Day (RR,D) by A10, A17, Th9, ORDINAL1:def 2;
reconsider R = Lr . E as Relation by A17, A11;
A19: Lp . E = ClosedProd (R,E,E) by A17, A10;
then RR /\ [:(BeforeGames E),(BeforeGames E):] = R /\ [:(BeforeGames E),(BeforeGames E):] by A11, A10, A6, Th24, A17;
then A20: x in ClosedProd (RR,E,E) by A16, A17, A19, Th15;
then consider y, z being object such that
A21: ( y in Day (RR,E) & z in Day (RR,E) & [y,z] = x ) by ZFMISC_1:def 2;
( ( born (RR,y) in E & born (RR,z) in E ) or ( born (RR,y) = E & born (RR,z) c= E ) or ( born (RR,y) c= E & born (RR,z) = E ) ) by A20, A21, Def10;
then ( born (RR,y) in D & born (RR,z) in D ) by ORDINAL1:10, ORDINAL1:12, A10, A17;
hence x in OpenProd (RR,D,{}) by A18, A21, Def9; :: thesis: verum

end;

OpenProd (RR,D,{}) c= union (rng Lp)

proof

let x, y be object ; :: according to RELAT_1:def 3 :: thesis: ( not [x,y] in OpenProd (RR,D,{}) or [x,y] in union (rng Lp) )
assume A22: [x,y] in OpenProd (RR,D,{}) ; :: thesis: [x,y] in union (rng Lp)
A23: ( x in Day (RR,D) & y in Day (RR,D) ) by A22, ZFMISC_1:87;
then A24: ( born (RR,x) in D & born (RR,y) in D ) by A22, Def9;

per cases ( born (RR,x) c= born (RR,y) or not born (RR,x) c= born (RR,y) ) ;

suppose A25: born (RR,x) c= born (RR,y) ; :: thesis: [x,y] in union (rng Lp)

set B = born (RR,y);
A26: Day (RR,(born (RR,x))) c= Day (RR,(born (RR,y))) by A25, Th9;
A27: ( x in Day (RR,(born (RR,x))) & y in Day (RR,(born (RR,y))) ) by A23, Def8;
consider R being Relation such that
A28: ( Lr . (born (RR,y)) = R & R preserves_No_Comparison_on ClosedProd (R,(born (RR,y)),(born (RR,y))) & R c= ClosedProd (R,(born (RR,y)),(born (RR,y))) ) by A24, A6;
A29: Lp . (born (RR,y)) = ClosedProd (R,(born (RR,y)),(born (RR,y))) by A24, A28, A10;
then RR /\ [:(BeforeGames (born (RR,y))),(BeforeGames (born (RR,y))):] = R /\ [:(BeforeGames (born (RR,y))),(BeforeGames (born (RR,y))):] by A24, A28, A11, A10, A6, Th24;
then A30: ClosedProd (RR,(born (RR,y)),(born (RR,y))) = ClosedProd (R,(born (RR,y)),(born (RR,y))) by Th15;
A31: [x,y] in ClosedProd (RR,(born (RR,y)),(born (RR,y))) by A25, Def10, A26, A27;
Lp . (born (RR,y)) in rng Lp by A24, A10, FUNCT_1:def 3;
hence [x,y] in union (rng Lp) by A30, A29, A31, TARSKI:def 4; :: thesis: verum

end;

suppose A32: not born (RR,x) c= born (RR,y) ; :: thesis: [x,y] in union (rng Lp)

set B = born (RR,x);
A33: Day (RR,(born (RR,y))) c= Day (RR,(born (RR,x))) by A32, Th9;
A34: ( y in Day (RR,(born (RR,y))) & x in Day (RR,(born (RR,x))) ) by A23, Def8;
consider R being Relation such that
A35: ( Lr . (born (RR,x)) = R & R preserves_No_Comparison_on ClosedProd (R,(born (RR,x)),(born (RR,x))) & R c= ClosedProd (R,(born (RR,x)),(born (RR,x))) ) by A24, A6;
A36: Lp . (born (RR,x)) = ClosedProd (R,(born (RR,x)),(born (RR,x))) by A24, A35, A10;
then RR /\ [:(BeforeGames (born (RR,x))),(BeforeGames (born (RR,x))):] = R /\ [:(BeforeGames (born (RR,x))),(BeforeGames (born (RR,x))):] by A24, A35, A11, A10, A6, Th24;
then A37: ClosedProd (RR,(born (RR,x)),(born (RR,x))) = ClosedProd (R,(born (RR,x)),(born (RR,x))) by Th15;
A38: [x,y] in ClosedProd (RR,(born (RR,x)),(born (RR,x))) by A32, A33, A34, Def10;
Lp . (born (RR,x)) in rng Lp by A24, A10, FUNCT_1:def 3;
hence [x,y] in union (rng Lp) by A37, A36, A38, TARSKI:def 4; :: thesis: verum

end;

end;

end;

then OpenProd (RR,D,{}) = union (rng Lp) by A15, XBOOLE_0:def 10;
hence ex R being Relation st
( R preserves_No_Comparison_on ClosedProd (R,D,B) & R c= ClosedProd (R,D,B) ) by A14, Th27; :: thesis: verum

end;

for D being Ordinal holds S₁[D] from ORDINAL1:sch 2(A1);
hence ex R being Relation st
( R preserves_No_Comparison_on ClosedProd (R,A,B) & R c= ClosedProd (R,A,B) ) ; :: thesis: verum