thus
( A is anti-discrete implies for x, y being Point of X st x in A & y in A holds

Cl {x} = Cl {y} ) :: thesis: ( ( for x, y being Point of X st x in A & y in A holds

Cl {x} = Cl {y} ) implies A is anti-discrete )

Cl {x} = Cl {y} ) implies A is anti-discrete ) :: thesis: verum

Cl {x} = Cl {y} ) :: thesis: ( ( for x, y being Point of X st x in A & y in A holds

Cl {x} = Cl {y} ) implies A is anti-discrete )

proof

thus
( ( for x, y being Point of X st x in A & y in A holds
assume A1:
A is anti-discrete
; :: thesis: for x, y being Point of X st x in A & y in A holds

Cl {x} = Cl {y}

let x, y be Point of X; :: thesis: ( x in A & y in A implies Cl {x} = Cl {y} )

assume that

A2: x in A and

A3: y in A ; :: thesis: Cl {x} = Cl {y}

A c= Cl {y} by A1, A3;

then {x} c= Cl {y} by A2, ZFMISC_1:31;

then A4: Cl {x} c= Cl {y} by TOPS_1:5;

A c= Cl {x} by A1, A2;

then {y} c= Cl {x} by A3, ZFMISC_1:31;

then Cl {y} c= Cl {x} by TOPS_1:5;

hence Cl {x} = Cl {y} by A4; :: thesis: verum

end;Cl {x} = Cl {y}

let x, y be Point of X; :: thesis: ( x in A & y in A implies Cl {x} = Cl {y} )

assume that

A2: x in A and

A3: y in A ; :: thesis: Cl {x} = Cl {y}

A c= Cl {y} by A1, A3;

then {x} c= Cl {y} by A2, ZFMISC_1:31;

then A4: Cl {x} c= Cl {y} by TOPS_1:5;

A c= Cl {x} by A1, A2;

then {y} c= Cl {x} by A3, ZFMISC_1:31;

then Cl {y} c= Cl {x} by TOPS_1:5;

hence Cl {x} = Cl {y} by A4; :: thesis: verum

Cl {x} = Cl {y} ) implies A is anti-discrete ) :: thesis: verum

proof

assume A5:
for x, y being Point of X st x in A & y in A holds

Cl {x} = Cl {y} ; :: thesis: A is anti-discrete

end;Cl {x} = Cl {y} ; :: thesis: A is anti-discrete

now :: thesis: for x being Point of X st x in A holds

A c= Cl {x}

hence
A is anti-discrete
; :: thesis: verumA c= Cl {x}

let x be Point of X; :: thesis: ( x in A implies A c= Cl {x} )

assume A6: x in A ; :: thesis: A c= Cl {x}

end;assume A6: x in A ; :: thesis: A c= Cl {x}

now :: thesis: for a being object st a in A holds

a in Cl {x}

hence
A c= Cl {x}
; :: thesis: veruma in Cl {x}

let a be object ; :: thesis: ( a in A implies a in Cl {x} )

assume A7: a in A ; :: thesis: a in Cl {x}

then reconsider y = a as Point of X ;

{y} c= Cl {y} by PRE_TOPC:18;

then y in Cl {y} by ZFMISC_1:31;

hence a in Cl {x} by A5, A6, A7; :: thesis: verum

end;assume A7: a in A ; :: thesis: a in Cl {x}

then reconsider y = a as Point of X ;

{y} c= Cl {y} by PRE_TOPC:18;

then y in Cl {y} by ZFMISC_1:31;

hence a in Cl {x} by A5, A6, A7; :: thesis: verum