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 x in ^^ A,X ; :: thesis: x in the Points of (G_ k,X)
then ex B1 being Subset of X st
( x = B1 & card B1 = (card A) + 1 & A c= B1 ) ;
hence x in the Points of (G_ k,X) by A2, A3; :: thesis: verum

end;

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