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} } ;
now :: thesis: for P being set st P in { (MaxADSet a) where a is Point of Y : a in {x} } holds
P c= MaxADSet x
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 ex a being Point of Y st
( P = MaxADSet a & a in {x} ) ;
hence P c= MaxADSet x by TARSKI:def 1; :: thesis: verum
end;
then A1: MaxADSet {x} c= MaxADSet x by ZFMISC_1:76;
x in {x} by TARSKI:def 1;
then MaxADSet x in { (MaxADSet a) where a is Point of Y : a in {x} } ;
then MaxADSet x c= MaxADSet {x} by ZFMISC_1:74;
hence MaxADSet x = MaxADSet {x} by A1; :: thesis: verum