let X be non empty TopSpace; :: thesis: for A, B being Subset of X st MaxADSet A = MaxADSet B holds
Cl A = Cl B
let A, B be Subset of X; :: thesis: ( MaxADSet A = MaxADSet B implies Cl A = Cl B )
assume MaxADSet A = MaxADSet B ; :: thesis: Cl A = Cl B
then A1: ( B c= MaxADSet A & A c= MaxADSet B ) by Th34;
( MaxADSet A c= Cl A & MaxADSet B c= Cl B ) by Th61;
then ( B c= Cl A & A c= Cl B ) by A1, XBOOLE_1:1;
then ( Cl B c= Cl A & Cl A c= Cl B ) by TOPS_1:31;
hence Cl A = Cl B by XBOOLE_0:def 10; :: thesis: verum