let Y be non empty TopStruct ; :: thesis: for A being non empty Subset of Y holds TopStruct(# the carrier of (MaxADSspace A), the topology of (MaxADSspace A) #) = TopStruct(# the carrier of (MaxADSspace (MaxADSet A)), the topology of (MaxADSspace (MaxADSet A)) #)
let A be non empty Subset of Y; :: thesis: TopStruct(# the carrier of (MaxADSspace A), the topology of (MaxADSspace A) #) = TopStruct(# the carrier of (MaxADSspace (MaxADSet A)), the topology of (MaxADSspace (MaxADSet A)) #)
A1: the carrier of (MaxADSspace (MaxADSet A)) = MaxADSet (MaxADSet A) by Def18;
the carrier of (MaxADSspace A) = MaxADSet A by Def18;
hence TopStruct(# the carrier of (MaxADSspace A), the topology of (MaxADSspace A) #) = TopStruct(# the carrier of (MaxADSspace (MaxADSet A)), the topology of (MaxADSspace (MaxADSet A)) #) by A1, Th33, TSEP_1:5; :: thesis: verum