X | ([#] X) is closed
_{1} being SubSpace of X st

( b_{1} is strict & b_{1} is closed & not b_{1} is empty )
; :: thesis: verum

proof

hence
ex b
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;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

( b