X | ([#] X) is open

proof

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

end;

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