theorem Th30: :: CARD_FIN:31

for F, Ch being Function
for x, y being object st x in Ch " {y} holds
Intersection (F,Ch,y) c= F . x