theorem Th21: :: SCMYCIEL:21

for n being Nat
for X being b₁ -at_most_dimensional set
for x being Element of X st x in X holds
card x <= n + 1