let S be RealUnitarySpace; :: thesis: for U being Subset of S
for V being Subset of (TopSpaceNorm (RUSp2RNSp S)) st U = V holds
( U is closed iff V is closed )
let U be Subset of S; :: thesis: for V being Subset of (TopSpaceNorm (RUSp2RNSp S)) st U = V holds
( U is closed iff V is closed )
let V be Subset of (TopSpaceNorm (RUSp2RNSp S)); :: thesis: ( U = V implies ( U is closed iff V is closed ) )
assume A1: U = V ; :: thesis: ( U is closed iff V is closed )
reconsider U1 = U as Subset of (RUSp2RNSp S) ;
( U1 is closed iff V is closed ) by A1, NORMSP_2:15;
hence ( U is closed iff V is closed ) ; :: thesis: verum