:: deftheorem defines STAR COMBGRAS:def 4 :
for k being Nat
for X being non empty set
for T being Subset of the Points of (G_ (k,X)) holds
( T is STAR iff ex S being Subset of X st
( card S = k - 1 & T = { A where A is Subset of X : ( card A = k & S c= A ) } ) );