theorem Th76: :: CARDFIL4:97

for X1, X2 being non empty set
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)