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

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

let A be Subset of Y; :: thesis: MaxADSet A = MaxADSet (MaxADSet A)

A1: MaxADSet (MaxADSet A) c= MaxADSet A

proof

MaxADSet A c= MaxADSet (MaxADSet A)
by Th32;
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;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

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