let X be finite set ; :: thesis: for x being set st x in X holds
card (X \ {x}) < card X
let x be set ; :: thesis: ( x in X implies card (X \ {x}) < card X )
assume A1: x in X ; :: thesis: card (X \ {x}) < card X
card X > 0 by A1;
then reconsider c1 = (card X) - 1 as Element of NAT by NAT_1:20;
c1 < c1 + 1 by NAT_1:13;
hence card (X \ {x}) < card X by A1, Th65; :: thesis: verum