let Y be non empty TopStruct ; :: thesis: for A, B being Subset of Y st A c= B holds
MaxADSet A c= MaxADSet B
let A, B be Subset of Y; :: thesis: ( A c= B implies MaxADSet A c= MaxADSet B )
set E = { (MaxADSet a) where a is Point of Y : a in A } ;
set F = { (MaxADSet b) where b is Point of Y : b in B } ;
assume A1: A c= B ; :: thesis: MaxADSet A c= MaxADSet B
{ (MaxADSet a) where a is Point of Y : a in A } c= { (MaxADSet b) where b is Point of Y : b in B }

proof

let C be object ; :: according to TARSKI:def 3 :: thesis: ( not C in { (MaxADSet a) where a is Point of Y : a in A } or C in { (MaxADSet b) where b is Point of Y : b in B } )
assume C in { (MaxADSet a) where a is Point of Y : a in A } ; :: thesis: C in { (MaxADSet b) where b is Point of Y : b in B }
then ex a being Point of Y st
( C = MaxADSet a & a in A ) ;
hence C in { (MaxADSet b) where b is Point of Y : b in B } by A1; :: thesis: verum

end;

hence MaxADSet A c= MaxADSet B by ZFMISC_1:77; :: thesis: verum