A3: the Points of (G_ k,X) = { B where B is Subset of X : card B = k } by A1, Def1;
^^ A,X c= the Points of (G_ k,X)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in ^^ A,X or x in the Points of (G_ k,X) )
assume A4: x in ^^ A,X ; :: thesis: x in the Points of (G_ k,X)
consider B1 being Subset of X such that
A5: ( x = B1 & card B1 = (card A) + 1 & A c= B1 ) by A4;
thus x in the Points of (G_ k,X) by A2, A3, A5; :: thesis: verum

end;

hence ^^ A,X is Subset of the Points of (G_ k,X) ; :: thesis: verum