let Y be non empty TopStruct ; :: thesis: for A, B being non empty Subset of Y holds
( ( B is Subset of (MaxADSspace A) & A is Subset of (MaxADSspace B) ) iff TopStruct(# the carrier of (MaxADSspace A),the topology of (MaxADSspace A) #) = TopStruct(# the carrier of (MaxADSspace B),the topology of (MaxADSspace B) #) )
let A, B be non empty Subset of Y; :: thesis: ( ( B is Subset of (MaxADSspace A) & A is Subset of (MaxADSspace B) ) iff TopStruct(# the carrier of (MaxADSspace A),the topology of (MaxADSspace A) #) = TopStruct(# the carrier of (MaxADSspace B),the topology of (MaxADSspace B) #) )
A1: ( the carrier of (MaxADSspace A) = MaxADSet A & the carrier of (MaxADSspace B) = MaxADSet B ) by Def19;
hence ( B is Subset of (MaxADSspace A) & A is Subset of (MaxADSspace B) implies TopStruct(# the carrier of (MaxADSspace A),the topology of (MaxADSspace A) #) = TopStruct(# the carrier of (MaxADSspace B),the topology of (MaxADSspace B) #) ) by Th37, TSEP_1:5; :: thesis: ( TopStruct(# the carrier of (MaxADSspace A),the topology of (MaxADSspace A) #) = TopStruct(# the carrier of (MaxADSspace B),the topology of (MaxADSspace B) #) implies ( B is Subset of (MaxADSspace A) & A is Subset of (MaxADSspace B) ) )
assume TopStruct(# the carrier of (MaxADSspace A),the topology of (MaxADSspace A) #) = TopStruct(# the carrier of (MaxADSspace B),the topology of (MaxADSspace B) #) ; :: thesis: ( B is Subset of (MaxADSspace A) & A is Subset of (MaxADSspace B) )
hence ( B is Subset of (MaxADSspace A) & A is Subset of (MaxADSspace B) ) by A1, Th34; :: thesis: verum