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

let A be Subset of Y; :: thesis: A c= MaxADSet A

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in MaxADSet A )

assume A1: x in A ; :: thesis: x in MaxADSet A

then reconsider a = x as Point of Y ;

{a} c= A by A1, ZFMISC_1:31;

then MaxADSet {a} c= MaxADSet A by Th31;

then A2: MaxADSet a c= MaxADSet A by Th28;

A3: a in {a} by TARSKI:def 1;

{a} c= MaxADSet a by Th12;

then {a} c= MaxADSet A by A2;

hence x in MaxADSet A by A3; :: thesis: verum

let A be Subset of Y; :: thesis: A c= MaxADSet A

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in MaxADSet A )

assume A1: x in A ; :: thesis: x in MaxADSet A

then reconsider a = x as Point of Y ;

{a} c= A by A1, ZFMISC_1:31;

then MaxADSet {a} c= MaxADSet A by Th31;

then A2: MaxADSet a c= MaxADSet A by Th28;

A3: a in {a} by TARSKI:def 1;

{a} c= MaxADSet a by Th12;

then {a} c= MaxADSet A by A2;

hence x in MaxADSet A by A3; :: thesis: verum