theorem Th0: :: NORMSP_3:2

for X being RealNormSpace
for R being Subset of X holds
( R is open iff R ` is closed ) ;