let V be RealUnitarySpace; :: thesis: for M being Subset of (TopUnitSpace V) st M = [#] V holds
( M is open & M is closed )
let M be Subset of (TopUnitSpace V); :: thesis: ( M = [#] V implies ( M is open & M is closed ) )
A1: [#] (TopUnitSpace V) = the carrier of TopStruct(# the carrier of V,(Family_open_set V) #) ;
assume M = [#] V ; :: thesis: ( M is open & M is closed )
hence ( M is open & M is closed ) by A1; :: thesis: verum