theorem Th25: :: BORSUK_1:25

for X, Y being non empty TopSpace
for t being Point of Y
for A being Subset of X st A is compact holds
for G being a_neighborhood of [:A,{t}:] ex V being a_neighborhood of A ex W being a_neighborhood of t st [:V,W:] c= G