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 }

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

hence
MaxADSet A c= MaxADSet B
by ZFMISC_1:77; :: thesis: verum
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;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