let Y be non empty TopStruct ; :: thesis: for x, y being Point of Y holds
( the carrier of (MaxADSspace x) misses the carrier of (MaxADSspace y) or TopStruct(# the carrier of (MaxADSspace x), the topology of (MaxADSspace x) #) = TopStruct(# the carrier of (MaxADSspace y), the topology of (MaxADSspace y) #) )
let x, y be Point of Y; :: thesis: ( the carrier of (MaxADSspace x) misses the carrier of (MaxADSspace y) or TopStruct(# the carrier of (MaxADSspace x), the topology of (MaxADSspace x) #) = TopStruct(# the carrier of (MaxADSspace y), the topology of (MaxADSspace y) #) )
assume A1: the carrier of (MaxADSspace x) meets the carrier of (MaxADSspace y) ; :: thesis: TopStruct(# the carrier of (MaxADSspace x), the topology of (MaxADSspace x) #) = TopStruct(# the carrier of (MaxADSspace y), the topology of (MaxADSspace y) #)
A2: the carrier of (MaxADSspace y) = MaxADSet y by Def17;
the carrier of (MaxADSspace x) = MaxADSet x by Def17;
hence TopStruct(# the carrier of (MaxADSspace x), the topology of (MaxADSspace x) #) = TopStruct(# the carrier of (MaxADSspace y), the topology of (MaxADSspace y) #) by A2, A1, Th22, TSEP_1:5; :: thesis: verum