theorem Th35: :: CARD_FIN:36

for x1, x2, y being set
for F, Ch being Function st {x1,x2} = Ch " {y} holds
Intersection (F,Ch,y) = (F . x1) /\ (F . x2)