let Y be non empty TopStruct ; 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; ( ( 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 B) = MaxADSet B
by Def18;
A2:
the carrier of (MaxADSspace A) = MaxADSet A
by Def18;
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 A1, Th35, TSEP_1:5; ( 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) #)
; ( 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 A2, A1, Th32; verum