theorem Th55: :: STIRL2_1:55

for k being Nat
for X, x being set st card X = k + 1 & x in X holds
card (X \ {x}) = k