X | ([#] X) is closed

proof

let A be Subset of X; :: according to BORSUK_1:def 11 :: thesis: ( A = the carrier of (X | ([#] X)) implies A is closed )
assume A = the carrier of (X | ([#] X)) ; :: thesis: A is closed
then A = [#] (X | ([#] X))
.= [#] X by PRE_TOPC:def 5 ;
hence A is closed ; :: thesis: verum

end;

hence ex b₁ being SubSpace of X st
( b₁ is strict & b₁ is closed & not b₁ is empty ) ; :: thesis: verum