let Y be Subset of X; :: thesis: Y is n -at_most_dimensional
let x be set ; :: according to SCMYCIEL:def 4 :: thesis: ( x in Y implies card x c= n + 1 )
assume x in Y ; :: thesis: card x c= n + 1
hence card x c= n + 1 by Lnatmost; :: thesis: verum