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 object ; :: 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