theorem Th24: :: PRE_CIRC:25

for D being finite set st card D = 1 holds
ex x being Element of D st D = {x}