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;
card X = c1 + 1 ;
then ( card (X \ {x}) = c1 & c1 < c1 + 1 ) by A1, Th65, NAT_1:13;
hence card (X \ {x}) < card X ; :: thesis: verum