let X be non empty TopSpace; :: thesis: for A being Subset of X holds Cl (MaxADSet A) = Cl A
let A be Subset of X; :: thesis: Cl (MaxADSet A) = Cl A
A1: Cl (MaxADSet A) c= Cl A by Th61, TOPS_1:5;
Cl A c= Cl (MaxADSet A) by Th34, PRE_TOPC:19;
hence Cl (MaxADSet A) = Cl A by A1, XBOOLE_0:def 10; :: thesis: verum