let T be non empty TopStruct ; :: thesis: for t being Point of T
for A being Subset of T st A = {t} holds
Sspace t = T | A
let t be Point of T; :: thesis: for A being Subset of T st A = {t} holds
Sspace t = T | A
let A be Subset of T; :: thesis: ( A = {t} implies Sspace t = T | A )
assume A1: A = {t} ; :: thesis: Sspace t = T | A
the carrier of (Sspace t) = {t} by TEX_2:def 2
.= [#] (T | A) by A1, PRE_TOPC:def 5
.= the carrier of (T | A) ;
hence Sspace t = T | A by TSEP_1:5; :: thesis: verum