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

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