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

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