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 )
A1: MaxADSet A c= Cl A by Th59;
A2: MaxADSet B c= Cl B by Th59;
assume A3: MaxADSet A = MaxADSet B ; :: thesis: Cl A = Cl B
then A c= MaxADSet B by Th32;
then A c= Cl B by A2;
then A4: Cl A c= Cl B by TOPS_1:5;
B c= MaxADSet A by A3, Th32;
then B c= Cl A by A1;
then Cl B c= Cl A by TOPS_1:5;
hence Cl A = Cl B by A4; :: thesis: verum