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

proof

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;

hence MaxADSet A c= G ; :: thesis: verum