let T be non empty TopSpace; :: thesis: for x, y being Point of (T_0-reflex T) st x <> y holds
ex V being Subset of (T_0-reflex T) st
( V is open & ( ( x in V & not y in V ) or ( y in V & not x in V ) ) )
set S = T_0-reflex T;
set F = T_0-canonical_map T;
assume ex x, y being Point of (T_0-reflex T) st
( not x = y & ( for V being Subset of (T_0-reflex T) holds
( not V is open or ( not ( x in V & not y in V ) & not ( y in V & not x in V ) ) ) ) ) ; :: thesis: contradiction
then consider x, y being Point of (T_0-reflex T) such that
A1: x <> y and
A2: for V being Subset of (T_0-reflex T) st V is open holds
( x in V iff y in V ) ;
reconsider x = x, y = y as Point of (space (Indiscernible T)) ;
consider p being Point of T such that
A3: (T_0-canonical_map T) . p = x by BORSUK_1:29;
consider q being Point of T such that
A4: (T_0-canonical_map T) . q = y by BORSUK_1:29;
for A being Subset of T st A is open holds
( p in A iff q in A )

proof

let A be Subset of T; :: thesis: ( A is open implies ( p in A iff q in A ) )
assume A5: A is open ; :: thesis: ( p in A iff q in A )
T_0-canonical_map T is open by Th8;
then A6: (T_0-canonical_map T) .: A is open by A5;
reconsider F = T_0-canonical_map T as Function of the carrier of T, the carrier of (T_0-reflex T) ;

hereby :: thesis: ( q in A implies p in A )

assume p in A ; :: thesis: q in A
then x in F .: A by A3, FUNCT_2:35;
then F . q in F .: A by A2, A4, A6;
then ex x being object st
( x in the carrier of T & x in A & F . q = F . x ) by FUNCT_2:64;
hence q in A by A5, Th6; :: thesis: verum

end;

assume q in A ; :: thesis: p in A
then y in F .: A by A4, FUNCT_2:35;
then F . p in F .: A by A2, A3, A6;
then ex x being object st
( x in the carrier of T & x in A & F . p = F . x ) by FUNCT_2:64;
hence p in A by A5, Th6; :: thesis: verum

end;

then [p,q] in Indiscernibility T by Def3;
hence contradiction by A1, A3, A4, Th5; :: thesis: verum