for X being RealUnitarySpace
for Y being Subset of X holds
( Y is open iff Y ` is closed )