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
proof
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;
hence MaxADSet A c= F ; :: thesis: verum