theorem Th23: :: PRE_CIRC:24

for D being finite set
for k being Nat st card D = k + 1 holds
ex x being Element of D ex C being Subset of D st
( D = C \/ {x} & card C = k )