let T, S be TopSpace; :: thesis: 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
let R be Refinement of T,S; :: thesis: for V being Subset of T
for W being Subset of R st W = V & V is open holds
W is open
let V be Subset of T; :: thesis: for W being Subset of R st W = V & V is open holds
W is open
let W be Subset of R; :: thesis: ( W = V & V is open implies W is open )
assume A1: W = V ; :: thesis: ( not V is open or W is open )
assume V in the topology of T ; :: according to PRE_TOPC:def 2 :: thesis: W is open
hence W is open by A1, Th19; :: thesis: verum