let y be set ; :: thesis: 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
let F, Ch be Function; :: thesis: ( not Intersection (F,Ch,y) is empty implies for x1, x2 being set st x1 in Ch " {y} & x2 in Ch " {y} holds
F . x1 meets F . x2 )
assume not Intersection (F,Ch,y) is empty ; :: thesis: for x1, x2 being set st x1 in Ch " {y} & x2 in Ch " {y} holds
F . x1 meets F . x2
then consider z being object such that
A1: z in Intersection (F,Ch,y) ;
let x1, x2 be set ; :: thesis: ( x1 in Ch " {y} & x2 in Ch " {y} implies F . x1 meets F . x2 )
assume that
A2: x1 in Ch " {y} and
A3: x2 in Ch " {y} ; :: thesis: F . x1 meets F . x2
Ch . x2 in {y} by A3, FUNCT_1:def 7;
then A4: Ch . x2 = y by TARSKI:def 1;
Ch . x1 in {y} by A2, FUNCT_1:def 7;
then A5: Ch . x1 = y by TARSKI:def 1;
x2 in dom Ch by A3, FUNCT_1:def 7;
then A6: z in F . x2 by A1, A4, Def2;
x1 in dom Ch by A2, FUNCT_1:def 7;
then z in F . x1 by A1, A5, Def2;
hence F . x1 meets F . x2 by A6, XBOOLE_0:3; :: thesis: verum