let X be non empty TopSpace; :: thesis: for P being Subset of X st P is closed holds
MaxADSet P = P
let P be Subset of X; :: thesis: ( P is closed implies MaxADSet P = P )
assume P is closed ; :: thesis: MaxADSet P = P
then ( Cl P = P & MaxADSet P c= Cl P & P c= MaxADSet P ) by Th34, Th61, PRE_TOPC:52;
hence MaxADSet P = P by XBOOLE_0:def 10; :: thesis: verum