theorem Th26: :: CARD_FIN:27

for X9 being set
for F, Ch being Function
for y being object holds Intersection (F,Ch,y) c= Intersection (F,(Ch | X9),y)