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 MaxADSet x c= MaxADSet {x} by ZFMISC_1:74;

hence MaxADSet x = MaxADSet {x} by A1; :: thesis: verum

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

then A1:
MaxADSet {x} c= MaxADSet x
by ZFMISC_1:76;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;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

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