theorem Th19: :: PRE_CIRC:20

for F being non empty finite set holds (card F) - 1 = (card F) -' 1