let S1, S2, T1, T2 be non empty TopSpace; :: thesis:
let R be Refinement of [:S1,T1:],[:S2,T2:]; :: thesis:
let R1 be Refinement of S1,S2; :: thesis:
let R2 be Refinement of T1,T2; :: thesis:
assume that
A1: the carrier of S1 = the carrier of S2 and
A2: the carrier of T1 = the carrier of T2 ; :: thesis:
A3: the carrier of [:S1,T1:] = [:the carrier of S1,the carrier of T1:] by BORSUK_1:def 5;
reconsider BS = INTERSECTION the topology of S1,the topology of S2 as Basis of R1 by A1, YELLOW_9:60;
reconsider BT = INTERSECTION the topology of T1,the topology of T2 as Basis of R2 by A2, YELLOW_9:60;
reconsider Bpr = { [:a,b:] where a is Subset of R1, b is Subset of R2 : ( a in BS & b in BT ) } as Basis of [:R1,R2:] by YELLOW_9:40;
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 5
.= [:the carrier of S1,the carrier of T1:] by A1, A2 ;
A5: the carrier of R1 = the carrier of S1 \/ the carrier of S2 by YELLOW_9:def 6
.= the carrier of S1 by A1 ;
the carrier of R2 = the carrier of T1 \/ the carrier of T2 by YELLOW_9:def 6
.= the carrier of T1 by A2 ;
hence A6: the carrier of [:R1,R2:] = the carrier of R by A4, A5, BORSUK_1:def 5; :: thesis:
set C = { ([: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 ) } ;
A7: { ([: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 A1, A2, Th48;
{ ([: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 ) } = Bpr

proof

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis:

let c be set ; :: 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
A8: c = [:U1,V1:] /\ [:U2,V2:] and
A9: ( U1 is open & U2 is open & V1 is open & V2 is open ) ;
A10: c = [:(U1 /\ U2),(V1 /\ V2):] by A8, ZFMISC_1:123;
( U1 in the topology of S1 & U2 in the topology of S2 & V1 in the topology of T1 & V2 in the topology of T2 ) by A9, PRE_TOPC:def 5;
then ( U1 /\ U2 in BS & V1 /\ V2 in BT ) by SETFAM_1:def 5;
hence c in Bpr by A10; :: thesis:

end;

let c be set ; :: according to TARSKI:def 3 :: thesis:
assume c in Bpr ; :: thesis:
then consider a being Subset of R1, b being Subset of R2 such that
A11: ( c = [:a,b:] & a in BS & b in BT ) ;
consider a1, a2 being set such that
A12: ( a1 in the topology of S1 & a2 in the topology of S2 & a = a1 /\ a2 ) by A11, SETFAM_1:def 5;
consider b1, b2 being set such that
A13: ( b1 in the topology of T1 & b2 in the topology of T2 & b = b1 /\ b2 ) by A11, SETFAM_1:def 5;
reconsider a1 = a1 as Subset of S1 by A12;
reconsider a2 = a2 as Subset of S2 by A12;
reconsider b1 = b1 as Subset of T1 by A13;
reconsider b2 = b2 as Subset of T2 by A13;
A14: ( a1 is open & a2 is open & b1 is open & b2 is open ) by A12, A13, PRE_TOPC:def 5;
c = [:a1,b1:] /\ [:a2,b2:] by A11, A12, A13, ZFMISC_1:123;
hence 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 ) } by A14; :: thesis:

end;

hence the topology of [:R1,R2:] = the topology of R by A6, A7, YELLOW_9:25; :: thesis: