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:] )
set R = the strict 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:]
then the carrier of [:R1,R2:] = the carrier of the strict Refinement of [:S1,T1:],[:S2,T2:] by Th49;
hence [:R1,R2:] is Refinement of [:S1,T1:],[:S2,T2:] by A1, Th49; :: thesis: verum