let A, O be Ordinal; :: thesis: for R being Relation
for o being object st o in Games O & not o in Day (R,O) holds
not o in Day (R,A)
let R be Relation; :: thesis: for o being object st o in Games O & not o in Day (R,O) holds
not o in Day (R,A)
let o be object ; :: thesis: ( o in Games O & not o in Day (R,O) implies not o in Day (R,A) )
defpred S₁[ Ordinal] means for x being object
for O being Ordinal st x in (Games O) \ (Day (R,O)) holds
not x in Day (R,$1);
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 x be object ; :: thesis: for O being Ordinal st x in (Games O) \ (Day (R,O)) holds
not x in Day (R,D)
let O be Ordinal; :: thesis: ( x in (Games O) \ (Day (R,O)) implies not x in Day (R,D) )
assume that
A3: x in (Games O) \ (Day (R,O)) and
A4: x in Day (R,D) ; :: thesis: contradiction
reconsider xD = x as Element of Games D by A4;
reconsider xO = x as Element of Games O by A3;
A5: ( L_ xD << R, R_ xD & ( for x being object st x in (L_ xD) \/ (R_ xD) holds
ex O being Ordinal st
( O in D & x in Day (R,O) ) ) ) by A4, Th7;
not xO in Day (R,O) by A3, XBOOLE_0:def 5;
then consider y being object such that
A6: ( y in (L_ xO) \/ (R_ xO) & ( for H being Ordinal st H in O holds
not y in Day (R,H) ) ) by A5, Th7;
consider H being Ordinal such that
A7: ( H in O & y in Games H ) by A6, Th4;
not y in Day (R,H) by A6, A7;
then A8: y in (Games H) \ (Day (R,H)) by A7, XBOOLE_0:def 5;
ex W being Ordinal st
( W in D & y in Day (R,W) ) by A6, A4, Th7;
hence contradiction by A8, A2; :: thesis: verum

end;

A9: for D being Ordinal holds S₁[D] from ORDINAL1:sch 2(A1);
assume ( o in Games O & not o in Day (R,O) ) ; :: thesis: not o in Day (R,A)
then o in (Games O) \ (Day (R,O)) by XBOOLE_0:def 5;
hence not o in Day (R,A) by A9; :: thesis: verum