for k being Nat
for X being non empty set st 0 < k & k + 1 c= card X holds
for A being POINT of (G_ (k,X))
for L being LINE of (G_ (k,X)) holds
( A on L iff A c= L )