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, Th55; :: thesis: verum

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, Th55; :: thesis: verum