let y be set ; :: thesis: for F, Ch being Function st not Intersection F,Ch,y is empty holds
Ch " {y} c= dom F
let F, Ch be Function; :: thesis: ( not Intersection F,Ch,y is empty implies Ch " {y} c= dom F )
assume not Intersection F,Ch,y is empty ; :: thesis: Ch " {y} c= dom F
then consider z being set such that
A1: z in Intersection F,Ch,y by XBOOLE_0:def 1;
assume not Ch " {y} c= dom F ; :: thesis: contradiction
then consider x being set such that
A2: ( x in Ch " {y} & not x in dom F ) by TARSKI:def 3;
Ch . x in {y} by A2, FUNCT_1:def 13;
then ( Ch . x = y & x in dom Ch ) by A2, FUNCT_1:def 13, TARSKI:def 1;
then z in F . x by A1, Def2;
hence contradiction by A2, FUNCT_1:def 4; :: thesis: verum