for S1, S2, T1, T2 being non empty TopSpace
for R being Refinement of [:S1,T1:],[:S2,T2:]
for R1 being Refinement of S1,S2
for R2 being Refinement of T1,T2 st the carrier of S1 = the carrier of S2 & the carrier of T1 = the carrier of T2 holds
( the carrier of [:R1,R2:] = the carrier of R & the topology of [:R1,R2:] = the topology of R )