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

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