let Y be non empty TopStruct ; :: thesis: for A being Subset of Y holds A c= MaxADSet A
let A be Subset of Y; :: thesis: A c= MaxADSet A

now

let x be set ; :: thesis: ( x in A implies x in MaxADSet A )
assume A1: x in A ; :: thesis: x in MaxADSet A
then reconsider a = x as Point of Y ;
{a} c= A by A1, ZFMISC_1:31;
then MaxADSet {a} c= MaxADSet A by Th33;
then A2: MaxADSet a c= MaxADSet A by Th30;
A3: a in {a} by TARSKI:def 1;
{a} c= MaxADSet a by Th14;
then {a} c= MaxADSet A by A2, XBOOLE_1:1;
hence x in MaxADSet A by A3; :: thesis: verum

end;

hence A c= MaxADSet A by TARSKI:def 3; :: thesis: verum