let Y be non empty TopStruct ; :: thesis: for A, B being Subset of Y st A c= MaxADSet B holds
MaxADSet A c= MaxADSet B
let A, B be Subset of Y; :: thesis: ( A c= MaxADSet B implies MaxADSet A c= MaxADSet B )
assume A c= MaxADSet B ; :: thesis: MaxADSet A c= MaxADSet B
then MaxADSet A c= MaxADSet (MaxADSet B) by Th31;
hence MaxADSet A c= MaxADSet B by Th33; :: thesis: verum