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

MaxADSet A c= G

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

assume A1: G is open ; :: thesis: ( not A c= G or MaxADSet A c= G )

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

MaxADSet A c= G

MaxADSet A c= G

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

assume A1: G is open ; :: thesis: ( not A c= G or MaxADSet A c= G )

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

MaxADSet A c= G

proof

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

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

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= G by A1, A2, A7, Th24;

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

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

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

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= G by A1, A2, A7, Th24;

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

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