let S1, S2, T1, T2 be non empty TopSpace; :: thesis:
let R be Refinement of [:S1,T1:],[:S2,T2:]; :: thesis:
assume A1: ( the carrier of S1 = the carrier of S2 & 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 ) } ;
A2: the carrier of [:S2,T2:] = [: the carrier of S2, the carrier of T2:] by BORSUK_1:def 2;
A3: the carrier of [:S1,T1:] = [: the carrier of S1, the carrier of T1:] by BORSUK_1:def 2;
then reconsider BST = INTERSECTION ( the topology of [:S1,T1:], the topology of [:S2,T2:]) as Basis of R by A1, A2, YELLOW_9:60;
A4: 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 2
.= [: the carrier of S1, the carrier of T1:] by A1 ;
{ ([: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

let c be object ; :: 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 ex U1 being Subset of S1 ex U2 being Subset of S2 ex V1 being Subset of T1 ex V2 being Subset of T2 st
( c = [:U1,V1:] /\ [:U2,V2:] & U1 is open & U2 is open & V1 is open & V2 is open ) ;
hence c in bool the carrier of R by A1, A2, A4; :: thesis:

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 ;
A5: 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 2;
A6: 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 2;
A7: 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 A8: 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
A9: X in BST and
A10: p in X and
A11: X c= A by A8, YELLOW_9:31;
consider X1, X2 being set such that
A12: X1 in the topology of [:S1,T1:] and
A13: X2 in the topology of [:S2,T2:] and
A14: X = X1 /\ X2 by A9, SETFAM_1:def 5;
consider F1 being Subset-Family of [:S1,T1:] such that
A15: X1 = union F1 and
A16: 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 A6, A12;
p in X1 by A10, A14, XBOOLE_0:def 4;
then consider G1 being set such that
A17: p in G1 and
A18: G1 in F1 by A15, TARSKI:def 4;
A19: 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 A16, A18;
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 A5, A13;
p in X2 by A10, A14, XBOOLE_0:def 4;
then consider G2 being set such that
A22: p in G2 and
A23: G2 in F2 by A20, TARSKI:def 4;
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, A23;
then consider K2 being Subset of S2, L2 being Subset of T2 such that
A24: G2 = [:K2,L2:] and
A25: ( K2 in the topology of S2 & L2 in the topology of T2 ) ;
A26: [:K2,L2:] c= X2 by A20, A23, A24, ZFMISC_1:74;
A27: ( K2 is open & L2 is open ) by A25;
consider K1 being Subset of S1, L1 being Subset of T1 such that
A28: G1 = [:K1,L1:] and
A29: ( K1 in the topology of S1 & L1 in the topology of T1 ) by A19;
reconsider a = [:K1,L1:] /\ [:K2,L2:] as Subset of R by A1, A4, BORSUK_1:def 2;
take a ; :: thesis:
( K1 is open & L1 is open ) by A29;
hence a in C1 by A27; :: thesis:
thus p in a by A17, A22, A28, A24, XBOOLE_0:def 4; :: thesis:
[:K1,L1:] c= X1 by A15, A18, A28, ZFMISC_1:74;
then a c= X by A14, A26, XBOOLE_1:27;
hence a c= A 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= the topology of R

proof

let c be object ; :: according to TARSKI:def 3 :: thesis:
A30: BST c= the topology of R by TOPS_2:64;
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
A31: c = [:U1,V1:] /\ [:U2,V2:] and
A32: U1 is open and
A33: U2 is open and
A34: V1 is open and
A35: V2 is open ;
[:U2,V2:] is open by A33, A35, BORSUK_1:6;
then A36: [:U2,V2:] in the topology of [:S2,T2:] ;
[:U1,V1:] is open by A32, A34, BORSUK_1:6;
then [:U1,V1:] in the topology of [:S1,T1:] ;
then c in BST by A31, A36, SETFAM_1:def 5;
hence c in the topology of R by A30; :: 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 A7, YELLOW_9:32; :: thesis: