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 )

hence contradiction by A1, A3, A4, Th5; :: thesis: verum

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

then
[p,q] in Indiscernibility T
by Def3;
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) ;

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;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
q in A
; :: thesis: p in Aassume
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;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

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

hence contradiction by A1, A3, A4, Th5; :: thesis: verum