theorem Th39: :: WAYBEL26:39

for X being finite set holds
( proj1 X is finite & proj2 X is finite )