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 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 )
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 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 )
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 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 )
let x be set ; :: thesis: ( [:{x}, the carrier of Y:] c= G implies 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 ) )
set y = the Point of Y;
A1: ( the carrier of [:X,Y:] = [: the carrier of X, the carrier of Y:] & [x, the Point of Y] in [:{x}, the carrier of Y:] ) by BORSUK_1:def 2, ZFMISC_1:105;
defpred S₁[ object , object ] 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 );
assume A2: [:{x}, the carrier of Y:] c= G ; :: thesis: 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 )
then [:{x}, the carrier of Y:] c= the carrier of [:X,Y:] by XBOOLE_1:1;
then reconsider x9 = x as Point of X by A1, ZFMISC_1:87;
A3: [:{x9}, the carrier of Y:] c= union (Base-Appr G) by A2, BORSUK_1:13;

A4: now :: thesis: for y being set st y in the carrier of Y holds
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 )

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 ) )
A5: x in {x9} by TARSKI:def 1;
assume 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 )
then [x,y] in [:{x9}, the carrier of Y:] by A5, ZFMISC_1:87;
then consider Z being set such that
A6: [x,y] in Z and
A7: Z in Base-Appr G by A3, 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 3;
then ex X1 being Subset of X ex Y1 being Subset of Y st
( Z = [:X1,Y1:] & [:X1,Y1:] c= G & X1 is open & Y1 is open ) by A7;
hence 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 A6; :: thesis: verum

end;

A8: for i being object st i in the carrier of Y holds
ex j being object st S₁[i,j]

proof

let i be object ; :: thesis: ( i in the carrier of Y implies ex j being object st S₁[i,j] )
assume i in the carrier of Y ; :: thesis: ex j being object st S₁[i,j]
then consider G1 being Subset of X, H1 being Subset of Y such that
A9: ( [x,i] in [:G1,H1:] & [:G1,H1:] c= G & G1 is open & H1 is open ) by A4;
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 A9;
hence ex j being object st S₁[i,j] ; :: thesis: verum

end;

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