let Y be non empty TopStruct ; for x, y being Point of Y holds
( y is Point of (MaxADSspace x) iff TopStruct(# the carrier of (MaxADSspace y), the topology of (MaxADSspace y) #) = TopStruct(# the carrier of (MaxADSspace x), the topology of (MaxADSspace x) #) )
let x, y be Point of Y; ( y is Point of (MaxADSspace x) iff TopStruct(# the carrier of (MaxADSspace y), the topology of (MaxADSspace y) #) = TopStruct(# the carrier of (MaxADSspace x), the topology of (MaxADSspace x) #) )
A1:
the carrier of (MaxADSspace x) = MaxADSet x
by Def17;
thus
( y is Point of (MaxADSspace x) implies TopStruct(# the carrier of (MaxADSspace y), the topology of (MaxADSspace y) #) = TopStruct(# the carrier of (MaxADSspace x), the topology of (MaxADSspace x) #) )
( TopStruct(# the carrier of (MaxADSspace y), the topology of (MaxADSspace y) #) = TopStruct(# the carrier of (MaxADSspace x), the topology of (MaxADSspace x) #) implies y is Point of (MaxADSspace x) )
assume A2:
TopStruct(# the carrier of (MaxADSspace y), the topology of (MaxADSspace y) #) = TopStruct(# the carrier of (MaxADSspace x), the topology of (MaxADSspace x) #)
; y is Point of (MaxADSspace x)
the carrier of (MaxADSspace y) = MaxADSet y
by Def17;
hence
y is Point of (MaxADSspace x)
by A2, Th21; verum