let A, B be Ordinal; :: thesis: ( A c= B implies BeforeGames A c= BeforeGames B )
assume A1: A c= B ; :: thesis: BeforeGames A c= BeforeGames B
let x, y be object ; :: according to RELAT_1:def 3 :: thesis: ( not [x,y] in BeforeGames A or [x,y] in BeforeGames B )
assume [x,y] in BeforeGames A ; :: thesis: [x,y] in BeforeGames B
then ex O being Ordinal st
( O in A & [x,y] in Games O ) by Def5;
hence [x,y] in BeforeGames B by A1, Def5; :: thesis: verum