let Y be non empty TopStruct ; :: thesis: for F, A being Subset of Y st F is closed & A c= F holds

MaxADSet A c= F

let F, A be Subset of Y; :: thesis: ( F is closed & A c= F implies MaxADSet A c= F )

assume A1: F is closed ; :: thesis: ( not A c= F or MaxADSet A c= F )

assume A2: A c= F ; :: thesis: MaxADSet A c= F

MaxADSet A c= F

MaxADSet A c= F

let F, A be Subset of Y; :: thesis: ( F is closed & A c= F implies MaxADSet A c= F )

assume A1: F is closed ; :: thesis: ( not A c= F or MaxADSet A c= F )

assume A2: A c= F ; :: thesis: MaxADSet A c= F

MaxADSet A c= F

proof

hence
MaxADSet A c= F
; :: thesis: verum
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in MaxADSet A or x in F )

assume A3: x in MaxADSet A ; :: thesis: x in F

then reconsider a = x as Point of Y ;

consider D being set such that

A4: a in D and

A5: D in { (MaxADSet b) where b is Point of Y : b in A } by A3, TARSKI:def 4;

consider b being Point of Y such that

A6: D = MaxADSet b and

A7: b in A by A5;

A8: MaxADSet a = MaxADSet b by A4, A6, Th21;

A9: {a} c= MaxADSet a by Th12;

MaxADSet b c= F by A1, A2, A7, Th23;

then {a} c= F by A8, A9;

hence x in F by ZFMISC_1:31; :: thesis: verum

end;assume A3: x in MaxADSet A ; :: thesis: x in F

then reconsider a = x as Point of Y ;

consider D being set such that

A4: a in D and

A5: D in { (MaxADSet b) where b is Point of Y : b in A } by A3, TARSKI:def 4;

consider b being Point of Y such that

A6: D = MaxADSet b and

A7: b in A by A5;

A8: MaxADSet a = MaxADSet b by A4, A6, Th21;

A9: {a} c= MaxADSet a by Th12;

MaxADSet b c= F by A1, A2, A7, Th23;

then {a} c= F by A8, A9;

hence x in F by ZFMISC_1:31; :: thesis: verum