theorem :: YELLOW12:50

for S1, S2, T1, T2 being non empty TopSpace
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
[:R1,R2:] is Refinement of [:S1,T1:],[:S2,T2:]