let B1, B2 be Subset of (Games A); :: thesis: ( ( for a being object holds
( a in B1 iff ex O being Ordinal st
( O in A & a in Games O ) ) ) & ( for a being object holds
( a in B2 iff ex O being Ordinal st
( O in A & a in Games O ) ) ) implies B1 = B2 )
assume that
A3: for x being object holds
( x in B1 iff ex O being Ordinal st
( O in A & x in Games O ) ) and
A4: for x being object holds
( x in B2 iff ex O being Ordinal st
( O in A & x in Games O ) ) ; :: thesis: B1 = B2

now :: thesis: for x being object holds
( x in B1 iff x in B2 )

let x be object ; :: thesis: ( x in B1 iff x in B2 )
( x in B1 iff ex O being Ordinal st
( O in A & x in Games O ) ) by A3;
hence ( x in B1 iff x in B2 ) by A4; :: thesis: verum

end;

hence B1 = B2 by TARSKI:2; :: thesis: verum