let x1, x2 be set ; :: thesis: for F, Ch1, Ch2 being Function st Ch1 " {x1} = Ch2 " {x2} holds
Intersection F,Ch1,x1 = Intersection F,Ch2,x2
let F be Function; :: thesis: for Ch1, Ch2 being Function st Ch1 " {x1} = Ch2 " {x2} holds
Intersection F,Ch1,x1 = Intersection F,Ch2,x2
let Ch1, Ch2 be Function; :: thesis: ( Ch1 " {x1} = Ch2 " {x2} implies Intersection F,Ch1,x1 = Intersection F,Ch2,x2 )
assume A1: Ch1 " {x1} = Ch2 " {x2} ; :: thesis: Intersection F,Ch1,x1 = Intersection F,Ch2,x2
thus Intersection F,Ch1,x1 c= Intersection F,Ch2,x2 :: according to XBOOLE_0:def 10 :: thesis: Intersection F,Ch2,x2 c= Intersection F,Ch1,x1

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in Intersection F,Ch1,x1 or z in Intersection F,Ch2,x2 )
assume A2: z in Intersection F,Ch1,x1 ; :: thesis: z in Intersection F,Ch2,x2

now

let x be set ; :: thesis: ( x in dom Ch2 & Ch2 . x = x2 implies z in F . x )
assume A3: ( x in dom Ch2 & Ch2 . x = x2 ) ; :: thesis: z in F . x
Ch2 . x in {x2} by A3, TARSKI:def 1;
then x in Ch1 " {x1} by A1, A3, FUNCT_1:def 13;
then ( x in dom Ch1 & Ch1 . x in {x1} ) by FUNCT_1:def 13;
then ( x in dom Ch1 & Ch1 . x = x1 ) by TARSKI:def 1;
hence z in F . x by A2, Def2; :: thesis: verum

end;

hence z in Intersection F,Ch2,x2 by A2, Def2; :: thesis: verum

end;

thus Intersection F,Ch2,x2 c= Intersection F,Ch1,x1 :: thesis: verum

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in Intersection F,Ch2,x2 or z in Intersection F,Ch1,x1 )
assume A4: z in Intersection F,Ch2,x2 ; :: thesis: z in Intersection F,Ch1,x1

now

let x be set ; :: thesis: ( x in dom Ch1 & Ch1 . x = x1 implies z in F . x )
assume A5: ( x in dom Ch1 & Ch1 . x = x1 ) ; :: thesis: z in F . x
Ch1 . x in {x1} by A5, TARSKI:def 1;
then x in Ch2 " {x2} by A1, A5, FUNCT_1:def 13;
then ( x in dom Ch2 & Ch2 . x in {x2} ) by FUNCT_1:def 13;
then ( x in dom Ch2 & Ch2 . x = x2 ) by TARSKI:def 1;
hence z in F . x by A4, Def2; :: thesis: verum

end;

hence z in Intersection F,Ch1,x1 by A4, Def2; :: thesis: verum

end;