for y being set
for F, Ch being Function st not Intersection (F,Ch,y) is empty holds
for x1, x2 being set st x1 in Ch " {y} & x2 in Ch " {y} holds
F . x1 meets F . x2