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 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, Th21;
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, Def17; :: thesis: verum
end;
assume A2: 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)
the carrier of (MaxADSspace y) = MaxADSet y by Def17;
hence y is Point of (MaxADSspace x) by A2, Th21; :: thesis: verum