let Y be non empty TopStruct ; :: thesis: for x being Point of Y holds MaxADSet x = MaxADSet {x}
let x be Point of Y; :: thesis: MaxADSet x = MaxADSet {x}
set M = { (MaxADSet a) where a is Point of Y : a in {x} } ;
x in {x} by TARSKI:def 1;
then MaxADSet x in { (MaxADSet a) where a is Point of Y : a in {x} } ;
then A1: MaxADSet x c= MaxADSet {x} by ZFMISC_1:92;

now

let P be set ; :: thesis: ( P in { (MaxADSet a) where a is Point of Y : a in {x} } implies P c= MaxADSet x )
assume P in { (MaxADSet a) where a is Point of Y : a in {x} } ; :: thesis: P c= MaxADSet x
then consider a being Point of Y such that
A2: P = MaxADSet a and
A3: a in {x} ;
thus P c= MaxADSet x by A2, A3, TARSKI:def 1; :: thesis: verum

end;

then MaxADSet {x} c= MaxADSet x by ZFMISC_1:94;
hence MaxADSet x = MaxADSet {x} by A1, XBOOLE_0:def 10; :: thesis: verum