let Y be non empty TopStruct ; :: thesis: 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; :: thesis: ( 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 & the carrier of (MaxADSspace y) = MaxADSet y ) 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) #) ) :: thesis: ( 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) )

proof

assume y is Point of (MaxADSspace x) ; :: thesis: TopStruct(# the carrier of (MaxADSspace y),the topology of (MaxADSspace y) #) = TopStruct(# the carrier of (MaxADSspace x),the topology of (MaxADSspace x) #)
then MaxADSet y = MaxADSet x by A1, Th23;
hence TopStruct(# the carrier of (MaxADSspace y),the topology of (MaxADSspace y) #) = TopStruct(# the carrier of (MaxADSspace x),the topology of (MaxADSspace x) #) by A1, TSEP_1:5; :: thesis: verum

end;

assume TopStruct(# the carrier of (MaxADSspace y),the topology of (MaxADSspace y) #) = TopStruct(# the carrier of (MaxADSspace x),the topology of (MaxADSspace x) #) ; :: thesis: y is Point of (MaxADSspace x)
hence y is Point of (MaxADSspace x) by A1, Th23; :: thesis: verum