let Y be non empty TopStruct ; for A being Subset of Y holds A c= MaxADSet A
let A be Subset of Y; A c= MaxADSet A
let x be object ; TARSKI:def 3 ( not x in A or x in MaxADSet A )
assume A1:
x in A
; 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 Th31;
then A2:
MaxADSet a c= MaxADSet A
by Th28;
A3:
a in {a}
by TARSKI:def 1;
{a} c= MaxADSet a
by Th12;
then
{a} c= MaxADSet A
by A2;
hence
x in MaxADSet A
by A3; verum