theorem Th48:
for
S1,
S2,
T1,
T2 being non
empty TopSpace for
R being
Refinement of
[:S1,T1:],
[:S2,T2:] st the
carrier of
S1 = the
carrier of
S2 & the
carrier of
T1 = the
carrier of
T2 holds
{ ([:U1,V1:] /\ [:U2,V2:]) where U1 is Subset of S1, U2 is Subset of S2, V1 is Subset of T1, V2 is Subset of T2 : ( U1 is open & U2 is open & V1 is open & V2 is open ) } is
Basis of
R