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))

^^ (A,X) c= the Points of (G_ (k,X))

proof

hence
^^ (A,X) is Subset of the Points of (G_ (k,X))
; :: thesis: verum
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;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