let Y be non empty TopStruct ; :: thesis: for A, B being non empty Subset of Y holds
( ( B is Subset of () & A is Subset of () ) iff TopStruct(# the carrier of (), the topology of () #) = TopStruct(# the carrier of (), the topology of () #) )

let A, B be non empty Subset of Y; :: thesis: ( ( B is Subset of () & A is Subset of () ) iff TopStruct(# the carrier of (), the topology of () #) = TopStruct(# the carrier of (), the topology of () #) )
A1: the carrier of () = MaxADSet B by Def18;
A2: the carrier of () = MaxADSet A by Def18;
hence ( B is Subset of () & A is Subset of () implies TopStruct(# the carrier of (), the topology of () #) = TopStruct(# the carrier of (), the topology of () #) ) by ; :: thesis: ( TopStruct(# the carrier of (), the topology of () #) = TopStruct(# the carrier of (), the topology of () #) implies ( B is Subset of () & A is Subset of () ) )
assume TopStruct(# the carrier of (), the topology of () #) = TopStruct(# the carrier of (), the topology of () #) ; :: thesis: ( B is Subset of () & A is Subset of () )
hence ( B is Subset of () & A is Subset of () ) by A2, A1, Th32; :: thesis: verum