let X be non empty TopSpace; :: thesis: 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 st
for i being set 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 )
let Y be non empty compact TopSpace; :: thesis: 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 st
for i being set 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 )
let G be open Subset of [:X,Y:]; :: thesis: for x being set st [:{x},the carrier of Y:] c= G holds
ex f being ManySortedSet of st
for i being set 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 )
let x be set ; :: thesis: ( [:{x},the carrier of Y:] c= G implies ex f being ManySortedSet of st
for i being set 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 ) )
assume A1: [:{x},the carrier of Y:] c= G ; :: thesis: ex f being ManySortedSet of st
for i being set 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 )
then A2: [:{x},the carrier of Y:] c= the carrier of [:X,Y:] by XBOOLE_1:1;
A3: the carrier of [:X,Y:] = [:the carrier of X,the carrier of Y:] by BORSUK_1:def 5;
consider y being Point of Y;
[x,y] in [:{x},the carrier of Y:] by ZFMISC_1:128;
then reconsider x' = x as Point of X by A2, A3, ZFMISC_1:106;
A4: [:{x'},the carrier of Y:] c= union (Base-Appr G) by A1, BORSUK_1:54;

A5: now

let y be set ; :: thesis: ( y in the carrier of Y implies ex G1 being Subset of X ex H1 being Subset of Y st
( [x,y] in [:G1,H1:] & [:G1,H1:] c= G & G1 is open & H1 is open ) )
assume A6: y in the carrier of Y ; :: thesis: ex G1 being Subset of X ex H1 being Subset of Y st
( [x,y] in [:G1,H1:] & [:G1,H1:] c= G & G1 is open & H1 is open )
x in {x'} by TARSKI:def 1;
then [x,y] in [:{x'},the carrier of Y:] by A6, ZFMISC_1:106;
then consider Z being set such that
A7: ( [x,y] in Z & Z in Base-Appr G ) by A4, TARSKI:def 4;
Base-Appr G = { [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( [:X1,Y1:] c= G & X1 is open & Y1 is open ) } by BORSUK_1:def 6;
then consider X1 being Subset of X, Y1 being Subset of Y such that
A8: ( Z = [:X1,Y1:] & [:X1,Y1:] c= G & X1 is open & Y1 is open ) by A7;
thus ex G1 being Subset of X ex H1 being Subset of Y st
( [x,y] in [:G1,H1:] & [:G1,H1:] c= G & G1 is open & H1 is open ) by A7, A8; :: thesis: verum

end;

defpred S₁[ set , set ] means ex G1 being Subset of X ex H1 being Subset of Y st
( $2 = [G1,H1] & [x,$1] in [:G1,H1:] & G1 is open & H1 is open & [:G1,H1:] c= G );
A9: for i being set st i in the carrier of Y holds
ex j being set st S₁[i,j]

proof

let i be set ; :: thesis: ( i in the carrier of Y implies ex j being set st S₁[i,j] )
assume i in the carrier of Y ; :: thesis: ex j being set st S₁[i,j]
then consider G1 being Subset of X, H1 being Subset of Y such that
A10: ( [x,i] in [:G1,H1:] & [:G1,H1:] c= G & G1 is open & H1 is open ) by A5;
ex G2 being Subset of X ex H2 being Subset of Y st
( [G1,H1] = [G2,H2] & [x,i] in [:G2,H2:] & G2 is open & H2 is open & [:G2,H2:] c= G ) by A10;
hence ex j being set st S₁[i,j] ; :: thesis: verum

end;

ex f being ManySortedSet of st
for i being set st i in the carrier of Y holds
S₁[i,f . i] from PBOOLE:sch 3(A9);
hence ex f being ManySortedSet of st
for i being set 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 ) ; :: thesis: verum