let T, S be TopSpace; :: thesis: ( the carrier of T = the carrier of S implies for R being Refinement of T,S
for V being Subset of T
for W being Subset of R st W = V & V is closed holds
W is closed )
assume A1: the carrier of T = the carrier of S ; :: 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 closed holds
W is closed
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 closed holds
W is closed
let V be Subset of T; :: thesis: for W being Subset of R st W = V & V is closed holds
W is closed
let W be Subset of R; :: thesis: ( W = V & V is closed implies W is closed )
assume A2: W = V ; :: thesis: ( not V is closed or W is closed )
assume V is closed ; :: thesis: W is closed
then A3: V ` is open ;
the carrier of R = the carrier of T \/ the carrier of S by YELLOW_9:def 6
.= the carrier of T by A1 ;
then W ` in the topology of T by A3, A2;
then W ` is open by Th19;
hence W is closed ; :: thesis: verum