let n be Nat; :: thesis: for X being n -at_most_dimensional set
for x being Element of X st x in X holds
card x <= n + 1
let X be n -at_most_dimensional set ; :: thesis: for x being Element of X st x in X holds
card x <= n + 1
let x be Element of X; :: thesis: ( x in X implies card x <= n + 1 )
assume x in X ; :: thesis: card x <= n + 1
then A1: card x c= n + 1 by Def4;
reconsider x = x as finite set ;
Segm (card x) c= Segm (n + 1) by A1;
hence card x <= n + 1 by NAT_1:39; :: thesis: verum