let X1, X2 be non empty set ; :: thesis:
let cB1 be filter_base of X1; :: thesis:
let cB2 be filter_base of X2; :: thesis:
let cF1 be Filter of X1; :: thesis:
let cF2 be Filter of X2; :: thesis:
let Y be non empty TopSpace; :: thesis:
let x be Point of Y; :: thesis:
let f be Function of [:X1,X2:],Y; :: thesis:
assume that
A1: x in lim_filter (f,<.cF1,cF2.)) and
A2: <.cB1.) = cF1 and
A3: <.cB2.) = cF2 ; :: thesis:
let U be a_neighborhood of x; :: thesis:
assume U is closed ; :: thesis:
then consider B1 being Element of cB1, B2 being Element of cB2 such that
A4: f .: [:B1,B2:] c= Int U by A1, A2, A3, Th75;
take B1 ; :: thesis:
take B2 ; :: thesis:
A5: for y being Element of B2 holds f .: [:B1,{y}:] c= Int U

let y be Element of B2; :: thesis:
[:B1,{y}:] c= [:B1,B2:] by ZFMISC_1:95;
then f .: [:B1,{y}:] c= f .: [:B1,B2:] by RELAT_1:125;
hence f .: [:B1,{y}:] c= Int U by A4; :: thesis:

end;

A6: for z being Element of B2
for y being Element of Y st y in lim_filter ((ProjMap2 (f,z)),cF1) holds
( filter_image ((ProjMap2 (f,z)),cF1) is proper Filter of (BoolePoset ([#] Y)) & Int U in filter_image ((ProjMap2 (f,z)),cF1) & y is_a_cluster_point_of filter_image ((ProjMap2 (f,z)),cF1),Y )

let z be Element of B2; :: thesis:
let y be Element of Y; :: thesis:
assume A7: y in lim_filter ((ProjMap2 (f,z)),cF1) ; :: thesis:
filter_image ((ProjMap2 (f,z)),cF1) is Filter of [#] Y by STRUCT_0:def 3;
hence filter_image ((ProjMap2 (f,z)),cF1) is proper Filter of (BoolePoset ([#] Y)) by Th17; :: thesis:
A8: (ProjMap2 (f,z)) " (Int U) is Subset of X1

dom (ProjMap2 (f,z)) = X1 by FUNCT_2:def 1;
hence (ProjMap2 (f,z)) " (Int U) is Subset of X1 by RELAT_1:132; :: thesis:

end;

A9: for z being Element of B2 holds (ProjMap2 (f,z)) .: B1 c= Int U

let z be Element of B2; :: thesis:
let t be object ; :: according to TARSKI:def 3 :: thesis:
assume t in (ProjMap2 (f,z)) .: B1 ; :: thesis:
then consider u being object such that
u in dom (ProjMap2 (f,z)) and
A10: u in B1 and
A11: t = (ProjMap2 (f,z)) . u by FUNCT_1:def 6;
(ProjMap2 (f,z)) . u = f . (u,z) by A10, MESFUNC9:def 7;
then A12: t = f . [u,z] by A11, BINOP_1:def 1;

[u,z] in [:X1,X2:] by A10, ZFMISC_1:def 2;
hence [u,z] in dom f by FUNCT_2:def 1; :: thesis:
( z in {z} & u in B1 ) by TARSKI:def 1, A10;
hence [u,z] in [:B1,{z}:] by ZFMISC_1:def 2; :: thesis:

end;

then VALB: t in f .: [:B1,{z}:] by A12, FUNCT_1:def 6;
f .: [:B1,{z}:] c= Int U by A5;
hence t in Int U by VALB; :: thesis:

end;

thus ( Int U in filter_image ((ProjMap2 (f,z)),cF1) & y is_a_cluster_point_of filter_image ((ProjMap2 (f,z)),cF1),Y ) :: thesis:

(ProjMap2 (f,z)) .: B1 c= Int U by A9;
then B1 c= (ProjMap2 (f,z)) " (Int U) by FUNCT_2:95;
then (ProjMap2 (f,z)) " (Int U) in cF1 by A2, A8, CARDFIL2:def 8;
hence Int U in filter_image ((ProjMap2 (f,z)),cF1) ; :: thesis:
thus y is_a_cluster_point_of filter_image ((ProjMap2 (f,z)),cF1),Y by A7, Th19; :: thesis:

end;

end;

for z being Element of B2
for y being Element of Y st y in lim_filter ((ProjMap2 (f,z)),cF1) holds
y in Cl (Int U)

let z be Element of B2; :: thesis:
let y be Element of Y; :: thesis:
assume y in lim_filter ((ProjMap2 (f,z)),cF1) ; :: thesis:
then ( filter_image ((ProjMap2 (f,z)),cF1) is proper Filter of (BoolePoset ([#] Y)) & Int U in filter_image ((ProjMap2 (f,z)),cF1) & y is_a_cluster_point_of filter_image ((ProjMap2 (f,z)),cF1),Y ) by A6;
hence y in Cl (Int U) by YELLOW19:25; :: thesis:

end;

hence for z being Element of X2
for y being Element of Y st z in B2 & y in lim_filter ((ProjMap2 (f,z)),cF1) holds
y in Cl (Int U) ; :: thesis: