let Y be non empty TopStruct ; :: thesis: for x being Point of Y holds TopStruct(# the carrier of (MaxADSspace x),the topology of (MaxADSspace x) #) = TopStruct(# the carrier of (MaxADSspace {x}),the topology of (MaxADSspace {x}) #)
let x be Point of Y; :: thesis: TopStruct(# the carrier of (MaxADSspace x),the topology of (MaxADSspace x) #) = TopStruct(# the carrier of (MaxADSspace {x}),the topology of (MaxADSspace {x}) #)
( the carrier of (MaxADSspace x) = MaxADSet x & the carrier of (MaxADSspace {x}) = MaxADSet {x} & MaxADSet x = MaxADSet {x} ) by Def17, Def19, Th30;
hence TopStruct(# the carrier of (MaxADSspace x),the topology of (MaxADSspace x) #) = TopStruct(# the carrier of (MaxADSspace {x}),the topology of (MaxADSspace {x}) #) by TSEP_1:5; :: thesis: verum