let Y be non empty TopStruct ; :: thesis: for Y0 being 1 -element SubSpace of Y ex y being Point of Y st TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of (Sspace y), the topology of (Sspace y) #)
let Y0 be 1 -element SubSpace of Y; :: thesis: ex y being Point of Y st TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of (Sspace y), the topology of (Sspace y) #)
consider y0 being Element of Y0 such that
A1: the carrier of Y0 = {y0} by TEX_1:def 1;
the carrier of Y0 is Subset of Y by Lm1;
then reconsider y = y0 as Point of Y by A1, ZFMISC_1:31;
take y ; :: thesis: TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of (Sspace y), the topology of (Sspace y) #)
the carrier of Y0 = the carrier of (Sspace y) by A1, Def2;
hence TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of (Sspace y), the topology of (Sspace y) #) by TSEP_1:5; :: thesis: verum