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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in MaxADSet (MaxADSet A) or x in MaxADSet A )
assume x in MaxADSet (MaxADSet A) ; :: thesis: x in MaxADSet A
then consider C being set such that
A2: x in C and
A3: C in { (MaxADSet a) where a is Point of Y : a in MaxADSet A } by TARSKI:def 4;
consider a being Point of Y such that
A4: C = MaxADSet a and
A5: a in MaxADSet A by A3;
consider D being set such that
A6: a in D and
A7: D in { (MaxADSet b) where b is Point of Y : b in A } by A5, TARSKI:def 4;
consider b being Point of Y such that
A8: D = MaxADSet b and
b in A by A7;
MaxADSet a = MaxADSet b by A6, A8, Th21;
hence x in MaxADSet A by A2, A4, A7, A8, TARSKI:def 4; :: thesis: verum

end;

MaxADSet A c= MaxADSet (MaxADSet A) by Th32;
hence MaxADSet A = MaxADSet (MaxADSet A) by A1; :: thesis: verum