let X be RealUnitarySpace; :: thesis: for Y being Subset of X holds
( Y is open iff Y ` is closed )
let Y be Subset of X; :: thesis: ( Y is open iff Y ` is closed )
thus ( Y is open implies Y ` is closed ) ; :: thesis: ( Y ` is closed implies Y is open )
assume Y ` is closed ; :: thesis: Y is open
then consider Z being Subset of (RUSp2RNSp X) such that
A2: ( Z = Y ` & Z is closed ) ;
Z ` is open by A2;
hence Y is open by A2; :: thesis: verum