let F, Ch be Function; for x, y being object st x in Ch " {y} holds
Intersection (F,Ch,y) c= F . x
let x, y be object ; ( x in Ch " {y} implies Intersection (F,Ch,y) c= F . x )
assume A1:
x in Ch " {y}
; 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 ; TARSKI:def 3 ( not z in Intersection (F,Ch,y) or z in F . x )
assume
z in Intersection (F,Ch,y)
; z in F . x
hence
z in F . x
by A2, A3, Def2; verum