theorem Th20: :: CARD_3:20

for x being object
for X being set holds card (pi (X,x)) c= card X