let A be non degenerated commutative Ring; :: thesis:
let P, Q be Point of (ZariskiTS A); :: thesis:
reconsider P1 = P, Q1 = Q as prime Ideal of A by Lm44;
assume P <> Q ; :: thesis:

per cases ;

suppose not Q c= P ; :: thesis:

then Q \ P <> {} by XBOOLE_1:37;
then consider x being object such that
A3: x in Q \ P by XBOOLE_0:def 1;
x in Q1 by A3;
then reconsider x = x as Element of A ;
PrimeIdeals (A,({x} -Ideal)) is closed Subset of (ZariskiTS A) by Def7;
then reconsider W = ([#] (ZariskiTS A)) \ (PrimeIdeals (A,({x} -Ideal))) as open Subset of (ZariskiTS A) by PRE_TOPC:def 3;
A5: not x in P by XBOOLE_0:def 5, A3;
A6: not P in PrimeIdeals (A,({x} -Ideal))

proof

assume P in PrimeIdeals (A,({x} -Ideal)) ; :: thesis:
then consider P0 being prime Ideal of A such that
A8: P = P0 and
A9: {x} -Ideal c= P0 ;
thus contradiction by A5, IDEAL_1:66, A8, A9; :: thesis:

end;

{x} -Ideal c= Q1 -Ideal by A3, ZFMISC_1:31, IDEAL_1:57;
then {x} -Ideal c= Q1 by IDEAL_1:44;
then Q in PrimeIdeals (A,({x} -Ideal)) ;
then ( P in W & not Q in W ) by A6, XBOOLE_0:def 5;
hence ex V being Subset of (ZariskiTS A) st
( V is open & ( ( P in V & not Q in V ) or ( Q in V & not P in V ) ) ) ; :: thesis:

end;

suppose ( Q c= P & Q <> P ) ; :: thesis:

then Q c< P ;
then consider x being object such that
A13: x in P and
A14: not x in Q by XBOOLE_0:6;
x in P1 by A13;
then reconsider x = x as Element of A ;
PrimeIdeals (A,({x} -Ideal)) is closed Subset of (ZariskiTS A) by Def7;
then reconsider W = ([#] (ZariskiTS A)) \ (PrimeIdeals (A,({x} -Ideal))) as open Subset of (ZariskiTS A) by PRE_TOPC:def 3;
A16: not Q in PrimeIdeals (A,({x} -Ideal))

proof

assume Q in PrimeIdeals (A,({x} -Ideal)) ; :: thesis:
then consider Q0 being prime Ideal of A such that
A18: Q = Q0 and
A19: {x} -Ideal c= Q0 ;
thus contradiction by A14, IDEAL_1:66, A18, A19; :: thesis:

end;

{x} -Ideal c= P1 -Ideal by A13, ZFMISC_1:31, IDEAL_1:57;
then {x} -Ideal c= P1 by IDEAL_1:44;
then P in PrimeIdeals (A,({x} -Ideal)) ;
then ( Q in W & not P in W ) by A16, XBOOLE_0:def 5;
hence ex V being Subset of (ZariskiTS A) st
( V is open & ( ( P in V & not Q in V ) or ( Q in V & not P in V ) ) ) ; :: thesis:

end;

end;