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