:: deftheorem Def4 defines -at_most_dimensional SCMYCIEL:def 4 :
for n being Nat
for X being set holds
( X is n -at_most_dimensional iff for x being set st x in X holds
card x c= n + 1 );