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 set such that
A1: z in Intersection F,Ch,y by XBOOLE_0:def 1;
let x1, x2 be set ; :: thesis: ( x1 in Ch " {y} & x2 in Ch " {y} implies F . x1 meets F . x2 )
assume A2: ( x1 in Ch " {y} & x2 in Ch " {y} ) ; :: thesis: F . x1 meets F . x2
( Ch . x1 in {y} & Ch . x2 in {y} ) by A2, FUNCT_1:def 13;
then ( Ch . x1 = y & x1 in dom Ch & Ch . x2 = y & x2 in dom Ch ) by A2, FUNCT_1:def 13, TARSKI:def 1;
then ( z in F . x1 & z in F . x2 ) by A1, Def2;
hence F . x1 meets F . x2 by XBOOLE_0:3; :: thesis: verum