let X1, X2 be non empty set ; :: thesis: for cB1 being filter_base of X1
for cB2 being filter_base of X2
for cF1 being Filter of X1
for cF2 being Filter of X2
for Y being non empty TopSpace
for x being Point of Y
for f being Function of [:X1,X2:],Y st x in lim_filter (f,<.cF1,cF2.)) & <.cB1.) = cF1 & <.cB2.) = cF2 holds
for U being a_neighborhood of x st U is closed holds
ex B1 being Element of cB1 ex B2 being Element of cB2 st
for z being Element of X1
for y being Element of Y st z in B1 & y in lim_filter ((ProjMap1 (f,z)),cF2) holds
y in Cl (Int U)

let cB1 be filter_base of X1; :: thesis: for cB2 being filter_base of X2
for cF1 being Filter of X1
for cF2 being Filter of X2
for Y being non empty TopSpace
for x being Point of Y
for f being Function of [:X1,X2:],Y st x in lim_filter (f,<.cF1,cF2.)) & <.cB1.) = cF1 & <.cB2.) = cF2 holds
for U being a_neighborhood of x st U is closed holds
ex B1 being Element of cB1 ex B2 being Element of cB2 st
for z being Element of X1
for y being Element of Y st z in B1 & y in lim_filter ((ProjMap1 (f,z)),cF2) holds
y in Cl (Int U)

let cB2 be filter_base of X2; :: thesis: for cF1 being Filter of X1
for cF2 being Filter of X2
for Y being non empty TopSpace
for x being Point of Y
for f being Function of [:X1,X2:],Y st x in lim_filter (f,<.cF1,cF2.)) & <.cB1.) = cF1 & <.cB2.) = cF2 holds
for U being a_neighborhood of x st U is closed holds
ex B1 being Element of cB1 ex B2 being Element of cB2 st
for z being Element of X1
for y being Element of Y st z in B1 & y in lim_filter ((ProjMap1 (f,z)),cF2) holds
y in Cl (Int U)

let cF1 be Filter of X1; :: thesis: for cF2 being Filter of X2
for Y being non empty TopSpace
for x being Point of Y
for f being Function of [:X1,X2:],Y st x in lim_filter (f,<.cF1,cF2.)) & <.cB1.) = cF1 & <.cB2.) = cF2 holds
for U being a_neighborhood of x st U is closed holds
ex B1 being Element of cB1 ex B2 being Element of cB2 st
for z being Element of X1
for y being Element of Y st z in B1 & y in lim_filter ((ProjMap1 (f,z)),cF2) holds
y in Cl (Int U)

let cF2 be Filter of X2; :: thesis: for Y being non empty TopSpace
for x being Point of Y
for f being Function of [:X1,X2:],Y st x in lim_filter (f,<.cF1,cF2.)) & <.cB1.) = cF1 & <.cB2.) = cF2 holds
for U being a_neighborhood of x st U is closed holds
ex B1 being Element of cB1 ex B2 being Element of cB2 st
for z being Element of X1
for y being Element of Y st z in B1 & y in lim_filter ((ProjMap1 (f,z)),cF2) holds
y in Cl (Int U)

let Y be non empty TopSpace; :: thesis: for x being Point of Y
for f being Function of [:X1,X2:],Y st x in lim_filter (f,<.cF1,cF2.)) & <.cB1.) = cF1 & <.cB2.) = cF2 holds
for U being a_neighborhood of x st U is closed holds
ex B1 being Element of cB1 ex B2 being Element of cB2 st
for z being Element of X1
for y being Element of Y st z in B1 & y in lim_filter ((ProjMap1 (f,z)),cF2) holds
y in Cl (Int U)

let x be Point of Y; :: thesis: for f being Function of [:X1,X2:],Y st x in lim_filter (f,<.cF1,cF2.)) & <.cB1.) = cF1 & <.cB2.) = cF2 holds
for U being a_neighborhood of x st U is closed holds
ex B1 being Element of cB1 ex B2 being Element of cB2 st
for z being Element of X1
for y being Element of Y st z in B1 & y in lim_filter ((ProjMap1 (f,z)),cF2) holds
y in Cl (Int U)

let f be Function of [:X1,X2:],Y; :: thesis: ( x in lim_filter (f,<.cF1,cF2.)) & <.cB1.) = cF1 & <.cB2.) = cF2 implies for U being a_neighborhood of x st U is closed holds
ex B1 being Element of cB1 ex B2 being Element of cB2 st
for z being Element of X1
for y being Element of Y st z in B1 & y in lim_filter ((ProjMap1 (f,z)),cF2) holds
y in Cl (Int U) )

assume that
A1: x in lim_filter (f,<.cF1,cF2.)) and
A2: <.cB1.) = cF1 and
A3: <.cB2.) = cF2 ; :: thesis: for U being a_neighborhood of x st U is closed holds
ex B1 being Element of cB1 ex B2 being Element of cB2 st
for z being Element of X1
for y being Element of Y st z in B1 & y in lim_filter ((ProjMap1 (f,z)),cF2) holds
y in Cl (Int U)

let U be a_neighborhood of x; :: thesis: ( U is closed implies ex B1 being Element of cB1 ex B2 being Element of cB2 st
for z being Element of X1
for y being Element of Y st z in B1 & y in lim_filter ((ProjMap1 (f,z)),cF2) holds
y in Cl (Int U) )

assume U is closed ; :: thesis: ex B1 being Element of cB1 ex B2 being Element of cB2 st
for z being Element of X1
for y being Element of Y st z in B1 & y in lim_filter ((ProjMap1 (f,z)),cF2) holds
y in Cl (Int U)

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: ex B2 being Element of cB2 st
for z being Element of X1
for y being Element of Y st z in B1 & y in lim_filter ((ProjMap1 (f,z)),cF2) holds
y in Cl (Int U)

take B2 ; :: thesis: for z being Element of X1
for y being Element of Y st z in B1 & y in lim_filter ((ProjMap1 (f,z)),cF2) holds
y in Cl (Int U)

A5: for y being Element of B1 holds f .: [:{y},B2:] c= Int U
proof
let y be Element of B1; :: thesis: f .: [:{y},B2:] c= Int U
[:{y},B2:] c= [:B1,B2:] by ZFMISC_1:95;
then f .: [:{y},B2:] c= f .: [:B1,B2:] by RELAT_1:125;
hence f .: [:{y},B2:] c= Int U by A4; :: thesis: verum
end;
A6: for z being Element of B1
for y being Element of Y st y in lim_filter ((ProjMap1 (f,z)),cF2) holds
( filter_image ((ProjMap1 (f,z)),cF2) is proper Filter of (BoolePoset ([#] Y)) & Int U in filter_image ((ProjMap1 (f,z)),cF2) & y is_a_cluster_point_of filter_image ((ProjMap1 (f,z)),cF2),Y )
proof
let z be Element of B1; :: thesis: for y being Element of Y st y in lim_filter ((ProjMap1 (f,z)),cF2) holds
( filter_image ((ProjMap1 (f,z)),cF2) is proper Filter of (BoolePoset ([#] Y)) & Int U in filter_image ((ProjMap1 (f,z)),cF2) & y is_a_cluster_point_of filter_image ((ProjMap1 (f,z)),cF2),Y )

let y be Element of Y; :: thesis: ( y in lim_filter ((ProjMap1 (f,z)),cF2) implies ( filter_image ((ProjMap1 (f,z)),cF2) is proper Filter of (BoolePoset ([#] Y)) & Int U in filter_image ((ProjMap1 (f,z)),cF2) & y is_a_cluster_point_of filter_image ((ProjMap1 (f,z)),cF2),Y ) )
assume A7: y in lim_filter ((ProjMap1 (f,z)),cF2) ; :: thesis: ( filter_image ((ProjMap1 (f,z)),cF2) is proper Filter of (BoolePoset ([#] Y)) & Int U in filter_image ((ProjMap1 (f,z)),cF2) & y is_a_cluster_point_of filter_image ((ProjMap1 (f,z)),cF2),Y )
filter_image ((ProjMap1 (f,z)),cF2) is Filter of [#] Y by STRUCT_0:def 3;
hence filter_image ((ProjMap1 (f,z)),cF2) is proper Filter of (BoolePoset ([#] Y)) by Th17; :: thesis: ( Int U in filter_image ((ProjMap1 (f,z)),cF2) & y is_a_cluster_point_of filter_image ((ProjMap1 (f,z)),cF2),Y )
A8: (ProjMap1 (f,z)) " (Int U) is Subset of X2
proof
dom (ProjMap1 (f,z)) = X2 by FUNCT_2:def 1;
hence (ProjMap1 (f,z)) " (Int U) is Subset of X2 by RELAT_1:132; :: thesis: verum
end;
A9: for z being Element of B1 holds (ProjMap1 (f,z)) .: B2 c= Int U
proof
let z be Element of B1; :: thesis: (ProjMap1 (f,z)) .: B2 c= Int U
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in (ProjMap1 (f,z)) .: B2 or t in Int U )
assume t in (ProjMap1 (f,z)) .: B2 ; :: thesis: t in Int U
then consider u being object such that
u in dom (ProjMap1 (f,z)) and
A10: u in B2 and
A11: t = (ProjMap1 (f,z)) . u by FUNCT_1:def 6;
(ProjMap1 (f,z)) . u = f . (z,u) by ;
then A12: t = f . [z,u] by ;
now :: thesis: ( [z,u] in dom f & [z,u] in [:{z},B2:] )
[z,u] in [:X1,X2:] by ;
hence [z,u] in dom f by FUNCT_2:def 1; :: thesis: [z,u] in [:{z},B2:]
( z in {z} & u in B2 ) by ;
hence [z,u] in [:{z},B2:] by ZFMISC_1:def 2; :: thesis: verum
end;
then A13: t in f .: [:{z},B2:] by ;
f .: [:{z},B2:] c= Int U by A5;
hence t in Int U by A13; :: thesis: verum
end;
thus ( Int U in filter_image ((ProjMap1 (f,z)),cF2) & y is_a_cluster_point_of filter_image ((ProjMap1 (f,z)),cF2),Y ) :: thesis: verum
proof
(ProjMap1 (f,z)) .: B2 c= Int U by A9;
then B2 c= (ProjMap1 (f,z)) " (Int U) by FUNCT_2:95;
then (ProjMap1 (f,z)) " (Int U) in cF2 by ;
hence Int U in filter_image ((ProjMap1 (f,z)),cF2) ; :: thesis: y is_a_cluster_point_of filter_image ((ProjMap1 (f,z)),cF2),Y
thus y is_a_cluster_point_of filter_image ((ProjMap1 (f,z)),cF2),Y by ; :: thesis: verum
end;
end;
for z being Element of B1
for y being Element of Y st y in lim_filter ((ProjMap1 (f,z)),cF2) holds
y in Cl (Int U)
proof
let z be Element of B1; :: thesis: for y being Element of Y st y in lim_filter ((ProjMap1 (f,z)),cF2) holds
y in Cl (Int U)

let y be Element of Y; :: thesis: ( y in lim_filter ((ProjMap1 (f,z)),cF2) implies y in Cl (Int U) )
assume y in lim_filter ((ProjMap1 (f,z)),cF2) ; :: thesis: y in Cl (Int U)
then ( filter_image ((ProjMap1 (f,z)),cF2) is proper Filter of (BoolePoset ([#] Y)) & Int U in filter_image ((ProjMap1 (f,z)),cF2) & y is_a_cluster_point_of filter_image ((ProjMap1 (f,z)),cF2),Y ) by A6;
hence y in Cl (Int U) by YELLOW19:25; :: thesis: verum
end;
hence for z being Element of X1
for y being Element of Y st z in B1 & y in lim_filter ((ProjMap1 (f,z)),cF2) holds
y in Cl (Int U) ; :: thesis: verum