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 A1: Cl P = P by PRE_TOPC:22;
A2: P c= MaxADSet P by Th32;
MaxADSet P c= Cl P by Th59;
hence MaxADSet P = P by A1, A2; :: thesis: verum