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