thus
( X is T_0 implies for x, y being Point of X holds

( not x <> y or not x in Cl {y} or not y in Cl {x} ) ) :: thesis: ( ( for x, y being Point of X holds

( not x <> y or not x in Cl {y} or not y in Cl {x} ) ) implies X is T_0 )

( not x <> y or not x in Cl {y} or not y in Cl {x} ) ; :: thesis: X is T_0

for x, y being Point of X st x <> y holds

Cl {x} <> Cl {y}

( not x <> y or not x in Cl {y} or not y in Cl {x} ) ) :: thesis: ( ( for x, y being Point of X holds

( not x <> y or not x in Cl {y} or not y in Cl {x} ) ) implies X is T_0 )

proof

assume A6:
for x, y being Point of X holds
assume A1:
X is T_0
; :: thesis: for x, y being Point of X holds

( not x <> y or not x in Cl {y} or not y in Cl {x} )

end;( not x <> y or not x in Cl {y} or not y in Cl {x} )

hereby :: thesis: verum

let x, y be Point of X; :: thesis: ( x <> y & x in Cl {y} implies not y in Cl {x} )

assume A2: x <> y ; :: thesis: ( x in Cl {y} implies not y in Cl {x} )

assume that

A3: x in Cl {y} and

A4: y in Cl {x} ; :: thesis: contradiction

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

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

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

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

then Cl {x} = Cl {y} by A5, XBOOLE_0:def 10;

hence contradiction by A1, A2; :: thesis: verum

end;assume A2: x <> y ; :: thesis: ( x in Cl {y} implies not y in Cl {x} )

assume that

A3: x in Cl {y} and

A4: y in Cl {x} ; :: thesis: contradiction

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

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

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

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

then Cl {x} = Cl {y} by A5, XBOOLE_0:def 10;

hence contradiction by A1, A2; :: thesis: verum

( not x <> y or not x in Cl {y} or not y in Cl {x} ) ; :: thesis: X is T_0

for x, y being Point of X st x <> y holds

Cl {x} <> Cl {y}

proof

hence
X is T_0
; :: thesis: verum
let x, y be Point of X; :: thesis: ( x <> y implies Cl {x} <> Cl {y} )

assume A7: x <> y ; :: thesis: Cl {x} <> Cl {y}

assume A8: Cl {x} = Cl {y} ; :: thesis: contradiction

hence contradiction ; :: thesis: verum

end;assume A7: x <> y ; :: thesis: Cl {x} <> Cl {y}

assume A8: Cl {x} = Cl {y} ; :: thesis: contradiction

hence contradiction ; :: thesis: verum