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 open iff V is open )
let U be Subset of S; :: thesis: for V being Subset of (TopSpaceNorm (RUSp2RNSp S)) st U = V holds
( U is open iff V is open )
let V be Subset of (TopSpaceNorm (RUSp2RNSp S)); :: thesis: ( U = V implies ( U is open iff V is open ) )
assume A1: U = V ; :: thesis: ( U is open iff V is open )
reconsider U1 = U as Subset of (RUSp2RNSp S) ;
( U1 is open iff V is open ) by A1, NORMSP_2:16;
hence ( U is open iff V is open ) ; :: thesis: verum