let S1, S2, T1, T2 be non empty TopSpace; :: thesis: 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:]
let R1 be Refinement of S1,S2; :: thesis: 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:]
let R2 be Refinement of T1,T2; :: thesis: ( the carrier of S1 = the carrier of S2 & the carrier of T1 = the carrier of T2 implies [:R1,R2:] is Refinement of [:S1,T1:],[:S2,T2:] )
assume A1: ( the carrier of S1 = the carrier of S2 & the carrier of T1 = the carrier of T2 ) ; :: thesis: [:R1,R2:] is Refinement of [:S1,T1:],[:S2,T2:]
consider R being strict Refinement of [:S1,T1:],[:S2,T2:];
[:R1,R2:] = R

proof

( the carrier of [:R1,R2:] = the carrier of R & the topology of [:R1,R2:] = the topology of R ) by A1, Th49;
hence [:R1,R2:] = R ; :: thesis: verum

end;

hence [:R1,R2:] is Refinement of [:S1,T1:],[:S2,T2:] ; :: thesis: verum