let A, B be Ordinal; :: thesis: for R being Relation st A c= B holds
Day (R,A) c= Day (R,B)
let R be Relation; :: thesis: ( A c= B implies Day (R,A) c= Day (R,B) )
assume A1: A c= B ; :: thesis: Day (R,A) c= Day (R,B)
let x1, x2 be object ; :: according to RELAT_1:def 3 :: thesis: ( not [x1,x2] in Day (R,A) or [x1,x2] in Day (R,B) )
set x = [x1,x2];
assume A2: [x1,x2] in Day (R,A) ; :: thesis: [x1,x2] in Day (R,B)
then A3: [x1,x2] in Games A ;
A4: ( L_ [x1,x2] << R, R_ [x1,x2] & ( for y being object st y in (L_ [x1,x2]) \/ (R_ [x1,x2]) holds
ex O being Ordinal st
( O in A & y in Day (R,O) ) ) ) by Th7, A2;
A5: Games A c= Games B by A1, Th1;
for y being object st y in (L_ [x1,x2]) \/ (R_ [x1,x2]) holds
ex O being Ordinal st
( O in B & y in Day (R,O) )

proof

let y be object ; :: thesis: ( y in (L_ [x1,x2]) \/ (R_ [x1,x2]) implies ex O being Ordinal st
( O in B & y in Day (R,O) ) )
assume y in (L_ [x1,x2]) \/ (R_ [x1,x2]) ; :: thesis: ex O being Ordinal st
( O in B & y in Day (R,O) )
then ex O being Ordinal st
( O in A & y in Day (R,O) ) by Th7, A2;
hence ex O being Ordinal st
( O in B & y in Day (R,O) ) by A1; :: thesis: verum

end;

hence [x1,x2] in Day (R,B) by A4, A5, A3, Th7; :: thesis: verum