consider L being Sequence such that
A1: ( Games A = L . A & dom L = succ A & ( for O being Ordinal st O in succ A holds
L . O = [:(bool (union (rng (L | O)))),(bool (union (rng (L | O)))):] ) ) by Def4;
L . A = [:(bool (union (rng (L | A)))),(bool (union (rng (L | A)))):] by A1, ORDINAL1:6;
hence ( not Games A is empty & Games A is Relation-like ) by A1; :: thesis: verum