let S1, S2, T1, T2 be non empty TopSpace; :: thesis:
let R be Refinement of [:S1,T1:],[:S2,T2:]; :: thesis:
assume that
A1: the carrier of S1 = the carrier of S2 and
A2: the carrier of T1 = the carrier of T2 ; :: thesis:
set Y = { ([:U1,V1:] /\ [:U2,V2:]) where U1 is Subset of S1, U2 is Subset of S2, V1 is Subset of T1, V2 is Subset of T2 : ( U1 is open & U2 is open & V1 is open & V2 is open ) } ;
A3: the carrier of [:S1,T1:] = [:the carrier of S1,the carrier of T1:] by BORSUK_1:def 5;
A4: the carrier of [:S2,T2:] = [:the carrier of S2,the carrier of T2:] by BORSUK_1:def 5;
then reconsider BST = INTERSECTION the topology of [:S1,T1:],the topology of [:S2,T2:] as Basis of R by A1, A2, A3, YELLOW_9:60;
A5: the topology of [:S1,T1:] = { (union A) where A is Subset-Family of [:S1,T1:] : A c= { [:X1,Y1:] where X1 is Subset of S1, Y1 is Subset of T1 : ( X1 in the topology of S1 & Y1 in the topology of T1 ) } } by BORSUK_1:def 5;
A6: the topology of [:S2,T2:] = { (union A) where A is Subset-Family of [:S2,T2:] : A c= { [:X1,Y1:] where X1 is Subset of S2, Y1 is Subset of T2 : ( X1 in the topology of S2 & Y1 in the topology of T2 ) } } by BORSUK_1:def 5;
A7: the carrier of R = the carrier of [:S1,T1:] \/ the carrier of [:S2,T2:] by YELLOW_9:def 6
.= [:the carrier of S1,the carrier of T1:] \/ [:the carrier of S2,the carrier of T2:] by A3, BORSUK_1:def 5
.= [:the carrier of S1,the carrier of T1:] by A1, A2 ;
A8: { ([:U1,V1:] /\ [:U2,V2:]) where U1 is Subset of S1, U2 is Subset of S2, V1 is Subset of T1, V2 is Subset of T2 : ( U1 is open & U2 is open & V1 is open & V2 is open ) } c= the topology of R

proof

let c be set ; :: according to TARSKI:def 3 :: thesis:
assume c in { ([:U1,V1:] /\ [:U2,V2:]) where U1 is Subset of S1, U2 is Subset of S2, V1 is Subset of T1, V2 is Subset of T2 : ( U1 is open & U2 is open & V1 is open & V2 is open ) } ; :: thesis:
then consider U1 being Subset of S1, U2 being Subset of S2, V1 being Subset of T1, V2 being Subset of T2 such that
A9: c = [:U1,V1:] /\ [:U2,V2:] and
A10: ( U1 is open & U2 is open & V1 is open & V2 is open ) ;
( [:U1,V1:] is open & [:U2,V2:] is open ) by A10, BORSUK_1:46;
then ( [:U1,V1:] in the topology of [:S1,T1:] & [:U2,V2:] in the topology of [:S2,T2:] ) by PRE_TOPC:def 5;
then A11: c in BST by A9, SETFAM_1:def 5;
BST c= the topology of R by CANTOR_1:def 2;
hence c in the topology of R by A11; :: thesis:

end;

{ ([:U1,V1:] /\ [:U2,V2:]) where U1 is Subset of S1, U2 is Subset of S2, V1 is Subset of T1, V2 is Subset of T2 : ( U1 is open & U2 is open & V1 is open & V2 is open ) } c= bool the carrier of R

proof

end;

then reconsider C1 = { ([:U1,V1:] /\ [:U2,V2:]) where U1 is Subset of S1, U2 is Subset of S2, V1 is Subset of T1, V2 is Subset of T2 : ( U1 is open & U2 is open & V1 is open & V2 is open ) } as Subset-Family of R ;
reconsider C1 = C1 as Subset-Family of R ;
for A being Subset of R st A is open holds
for p being Point of R st p in A holds
ex a being Subset of R st
( a in C1 & p in a & a c= A )

proof

let A be Subset of R; :: thesis:
assume A13: A is open ; :: thesis:
let p be Point of R; :: thesis:
assume p in A ; :: thesis:
then consider X being Subset of R such that
A14: ( X in BST & p in X & X c= A ) by A13, YELLOW_9:31;
consider X1, X2 being set such that
A15: X1 in the topology of [:S1,T1:] and
A16: X2 in the topology of [:S2,T2:] and
A17: X = X1 /\ X2 by A14, SETFAM_1:def 5;
consider F1 being Subset-Family of [:S1,T1:] such that
A18: X1 = union F1 and
A19: F1 c= { [:K1,L1:] where K1 is Subset of S1, L1 is Subset of T1 : ( K1 in the topology of S1 & L1 in the topology of T1 ) } by A5, A15;
consider F2 being Subset-Family of [:S2,T2:] such that
A20: X2 = union F2 and
A21: F2 c= { [:K2,L2:] where K2 is Subset of S2, L2 is Subset of T2 : ( K2 in the topology of S2 & L2 in the topology of T2 ) } by A6, A16;
A22: ( p in X1 & p in X2 ) by A14, A17, XBOOLE_0:def 4;
then consider G1 being set such that
A23: ( p in G1 & G1 in F1 ) by A18, TARSKI:def 4;
consider G2 being set such that
A24: ( p in G2 & G2 in F2 ) by A20, A22, TARSKI:def 4;
G1 in { [:K1,L1:] where K1 is Subset of S1, L1 is Subset of T1 : ( K1 in the topology of S1 & L1 in the topology of T1 ) } by A19, A23;
then consider K1 being Subset of S1, L1 being Subset of T1 such that
A25: G1 = [:K1,L1:] and
A26: ( K1 in the topology of S1 & L1 in the topology of T1 ) ;
G2 in { [:K2,L2:] where K2 is Subset of S2, L2 is Subset of T2 : ( K2 in the topology of S2 & L2 in the topology of T2 ) } by A21, A24;
then consider K2 being Subset of S2, L2 being Subset of T2 such that
A27: G2 = [:K2,L2:] and
A28: ( K2 in the topology of S2 & L2 in the topology of T2 ) ;
reconsider a = [:K1,L1:] /\ [:K2,L2:] as Subset of R by A1, A2, A7, BORSUK_1:def 5;
take a ; :: thesis:
( K1 is open & K2 is open & L1 is open & L2 is open ) by A26, A28, PRE_TOPC:def 5;
hence a in C1 ; :: thesis:
thus p in a by A23, A24, A25, A27, XBOOLE_0:def 4; :: thesis:
( [:K1,L1:] c= X1 & [:K2,L2:] c= X2 ) by A18, A20, A23, A24, A25, A27, ZFMISC_1:92;
then a c= X by A17, XBOOLE_1:27;
hence a c= A by A14, XBOOLE_1:1; :: thesis:

end;

hence { ([:U1,V1:] /\ [:U2,V2:]) where U1 is Subset of S1, U2 is Subset of S2, V1 is Subset of T1, V2 is Subset of T2 : ( U1 is open & U2 is open & V1 is open & V2 is open ) } is Basis of R by A8, YELLOW_9:32; :: thesis: