for X being non empty TopSpace
for Y being non empty compact TopSpace
for G being open Subset of [:X,Y:]
for x being set st [:{x}, the carrier of Y:] c= G holds
ex f being ManySortedSet of the carrier of Y st
for i being object st i in the carrier of Y holds
ex G1 being Subset of X ex H1 being Subset of Y st
( f . i = [G1,H1] & [x,i] in [:G1,H1:] & G1 is open & H1 is open & [:G1,H1:] c= G )