defpred S₁[ object ] means ex O being Ordinal st
( O in A & $1 in Games O );
consider X being set such that
A1: for x being object holds
( x in X iff ( x in Games A & S₁[x] ) ) from XBOOLE_0:sch 1();
X c= Games A

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in Games A )
thus ( not x in X or x in Games A ) by A1; :: thesis: verum

end;

then reconsider X = X as Subset of (Games A) ;
take X ; :: thesis: for a being object holds
( a in X iff ex O being Ordinal st
( O in A & a in Games O ) )
let x be object ; :: thesis: ( x in X iff ex O being Ordinal st
( O in A & x in Games O ) )
thus ( x in X implies ex O being Ordinal st
( O in A & x in Games O ) ) by A1; :: thesis: ( ex O being Ordinal st
( O in A & x in Games O ) implies x in X )
given O being Ordinal such that A2: ( O in A & x in Games O ) ; :: thesis: x in X
Games O c= Games A by A2, Th1, ORDINAL1:def 2;
hence x in X by A2, A1; :: thesis: verum