let F, Ch be Function; :: thesis: for x, y being object st x in Ch " {y} holds
Intersection (F,Ch,y) c= F . x
let x, y be object ; :: thesis: ( x in Ch " {y} implies Intersection (F,Ch,y) c= F . x )
assume A1: x in Ch " {y} ; :: thesis: Intersection (F,Ch,y) c= F . x
then A2: x in dom Ch by FUNCT_1:def 7;
Ch . x in {y} by A1, FUNCT_1:def 7;
then A3: Ch . x = y by TARSKI:def 1;
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in Intersection (F,Ch,y) or z in F . x )
assume z in Intersection (F,Ch,y) ; :: thesis: z in F . x
hence z in F . x by A2, A3, Def2; :: thesis: verum