for T, S being TopSpace
for R being Refinement of T,S
for V being Subset of T
for W being Subset of R st W = V & V is open holds
W is open by Th19;