:: deftheorem Def1 defines G_ COMBGRAS:def 1 :
for k being Nat
for X being non empty set st 0 < k & k + 1 c= card X holds
for b₃ being strict PartialLinearSpace holds
( b₃ = G_ (k,X) iff ( the Points of b₃ = { A where A is Subset of X : card A = k } & the Lines of b₃ = { L where L is Subset of X : card L = k + 1 } & the Inc of b₃ = (RelIncl (bool X)) /\ [: the Points of b₃, the Lines of b₃:] ) );