let X be set ; :: thesis: ( X is n -at_most_dimensional implies X is finite-membered )
assume A1: X is n -at_most_dimensional ; :: thesis: X is finite-membered
thus X is finite-membered :: thesis: verum

proof

let x be set ; :: according to FINSET_1:def 6 :: thesis: ( not x in X or x is finite )
assume x in X ; :: thesis: x is finite
then card x c= n + 1 by A1;
hence x is finite ; :: thesis: verum

end;