set F = the open closed Subset of (LinearTopSpaceNorm X);
reconsider G = the open closed Subset of (LinearTopSpaceNorm X) as Subset of X by NORMSP_2:def 4;
take G ; :: thesis: ( G is open & G is closed )
thus ( G is open & G is closed ) by NORMSP_2:32, NORMSP_2:33; :: thesis: verum