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 b1 being SubSpace of X st
( b1 is strict & b1 is open & not b1 is empty ) ; :: thesis: verum