theorem Th49:
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 )