theorem :: COMBGRAS:27

for k being Element of NAT
for X being non empty set st 0 < k & k + 1 c= card X holds
for T being Subset of the Points of (G_ (k,X)) st T is STAR holds
for S being Subset of X st S = meet T holds
( card S = k - 1 & T = { A where A is Subset of X : ( card A = k & S c= A ) } )