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

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