theorem Th30: :: COMBGRAS:30

for k being Element of NAT
for X being non empty set st k + 1 c= card X holds
for A being finite Subset of X st card A = k - 1 holds
meet (^^ (A,X,k)) = A