:: T_0TOPSP semantic presentation

begin

theorem Th1: :: T_0TOPSP:1
for X, Y being non empty set
for f being Function of X,Y
for A being Subset of X st ( for x1, x2 being Element of X st x1 in A & f . x1 = f . x2 holds
x2 in A ) holds
f " (f .: A) = A
proof
let X, Y be non empty set ; ::_thesis: for f being Function of X,Y
for A being Subset of X st ( for x1, x2 being Element of X st x1 in A & f . x1 = f . x2 holds
x2 in A ) holds
f " (f .: A) = A
let f be Function of X,Y; ::_thesis: for A being Subset of X st ( for x1, x2 being Element of X st x1 in A & f . x1 = f . x2 holds
x2 in A ) holds
f " (f .: A) = A
let A be Subset of X; ::_thesis: ( ( for x1, x2 being Element of X st x1 in A & f . x1 = f . x2 holds
x2 in A ) implies f " (f .: A) = A )
assume A1: for x1, x2 being Element of X st x1 in A & f . x1 = f . x2 holds
x2 in A ; ::_thesis: f " (f .: A) = A
 for x being set st x in f " (f .: A) holds
x in A
proof
let x be set ; ::_thesis: ( x in f " (f .: A) implies x in A )
assume A2: x in f " (f .: A) ; ::_thesis: x in A
then  f . x in f .: A by FUNCT_1:def_7;
then  ex x0 being set st
( x0 in X & x0 in A & f . x = f . x0 ) by FUNCT_2:64;
hence  x in A by A1, A2; ::_thesis: verum
end;
then  ( A c= f " (f .: A) & f " (f .: A) c= A ) by FUNCT_2:42, TARSKI:def_3;
hence  f " (f .: A) = A by XBOOLE_0:def_10; ::_thesis: verum
end;

definition
let T, S be TopStruct ;
predT,S are_homeomorphic  means :: T_0TOPSP:def 1
 ex f being Function of T,S st f is being_homeomorphism ;
end;

:: deftheorem  defines are_homeomorphic T_0TOPSP:def_1_:_
 for T, S being TopStruct holds
( T,S are_homeomorphic iff ex f being Function of T,S st f is being_homeomorphism );

definition
let T, S be TopStruct ;
let f be Function of T,S;
attrf is open  means :Def2: :: T_0TOPSP:def 2
 for A being Subset of T st A is open holds
f .: A is open ;
correctness
;
end;

:: deftheorem Def2 defines open T_0TOPSP:def_2_:_
 for T, S being TopStruct
for f being Function of T,S holds
( f is open iff for A being Subset of T st A is open holds
f .: A is open );

definition
let T be non empty TopStruct ;
func Indiscernibility T ->  Equivalence_Relation of the carrier of T means :Def3: :: T_0TOPSP:def 3
 for p, q being Point of T holds
( [p,q] in it iff for A being Subset of T st A is open holds
( p in A iff q in A ) );
existence
 ex b1 being Equivalence_Relation of the carrier of T st
for p, q being Point of T holds
( [p,q] in b1 iff for A being Subset of T st A is open holds
( p in A iff q in A ) )
proof
defpred S1[ set , set ] means  for A being Subset of T st A is open holds
( $1 in A iff $2 in A );
consider R being Relation of the carrier of T, the carrier of T such that
A1: for p, q being Element of T holds
( [p,q] in R iff S1[p,q] ) from RELSET_1:sch_2();
A2: R is_transitive_in the carrier of T
proof
let x, y, z be set ; :: according to RELAT_2:def_8 ::_thesis: ( not x in the carrier of T or not y in the carrier of T or not z in the carrier of T or not [x,y] in R or not [y,z] in R or [x,z] in R )
assume that
A3: ( x in the carrier of T & y in the carrier of T & z in the carrier of T ) and
A4: [x,y] in R and
A5: [y,z] in R ; ::_thesis: [x,z] in R
reconsider x9 = x, y9 = y, z9 = z as Element of T by A3;
 for A being Subset of T st A is open holds
( x9 in A iff z9 in A )
proof
let A be Subset of T; ::_thesis: ( A is open implies ( x9 in A iff z9 in A ) )
assume A6: A is open ; ::_thesis: ( x9 in A iff z9 in A )
then  ( x9 in A iff y9 in A ) by A1, A4;
hence  ( x9 in A iff z9 in A ) by A1, A5, A6; ::_thesis: verum
end;
hence  [x,z] in R by A1; ::_thesis: verum
end;
 R is_reflexive_in the carrier of T
proof
let x be set ; :: according to RELAT_2:def_1 ::_thesis: ( not x in the carrier of T or [x,x] in R )
A7: for A being Subset of T st A is open holds
( x in A iff x in A ) ;
assume  x in the carrier of T ; ::_thesis: [x,x] in R
hence  [x,x] in R by A1, A7; ::_thesis: verum
end;
then A8: ( dom R = the carrier of T & field R = the carrier of T ) by ORDERS_1:13;
 R is_symmetric_in the carrier of T
proof
let x, y be set ; :: according to RELAT_2:def_3 ::_thesis: ( not x in the carrier of T or not y in the carrier of T or not [x,y] in R or [y,x] in R )
assume that
A9: ( x in the carrier of T & y in the carrier of T ) and
A10: [x,y] in R ; ::_thesis: [y,x] in R
 for A being Subset of T st A is open holds
( y in A iff x in A ) by A1, A9, A10;
hence  [y,x] in R by A1, A9; ::_thesis: verum
end;
then reconsider R = R as Equivalence_Relation of the carrier of T by A8, A2, PARTFUN1:def_2, RELAT_2:def_11, RELAT_2:def_16;
take  R ; ::_thesis: for p, q being Point of T holds
( [p,q] in R iff for A being Subset of T st A is open holds
( p in A iff q in A ) )
let p, q be Point of T; ::_thesis: ( [p,q] in R iff for A being Subset of T st A is open holds
( p in A iff q in A ) )
thus  ( [p,q] in R implies for A being Subset of T st A is open holds
( p in A iff q in A ) ) by A1; ::_thesis: ( ( for A being Subset of T st A is open holds
( p in A iff q in A ) ) implies [p,q] in R )
assume  for A being Subset of T st A is open holds
( p in A iff q in A ) ; ::_thesis: [p,q] in R
hence  [p,q] in R by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Equivalence_Relation of the carrier of T st ( for p, q being Point of T holds
( [p,q] in b1 iff for A being Subset of T st A is open holds
( p in A iff q in A ) ) ) & ( for p, q being Point of T holds
( [p,q] in b2 iff for A being Subset of T st A is open holds
( p in A iff q in A ) ) ) holds
b1 = b2
proof
let R1, R2 be Equivalence_Relation of the carrier of T; ::_thesis: ( ( for p, q being Point of T holds
( [p,q] in R1 iff for A being Subset of T st A is open holds
( p in A iff q in A ) ) ) & ( for p, q being Point of T holds
( [p,q] in R2 iff for A being Subset of T st A is open holds
( p in A iff q in A ) ) ) implies R1 = R2 )
assume that
A11: for p, q being Point of T holds
( [p,q] in R1 iff for A being Subset of T st A is open holds
( p in A iff q in A ) ) and
A12: for p, q being Point of T holds
( [p,q] in R2 iff for A being Subset of T st A is open holds
( p in A iff q in A ) ) ; ::_thesis: R1 = R2
let x, y be Point of T; :: according to RELSET_1:def_2 ::_thesis: ( ( not [x,y] in R1 or [x,y] in R2 ) & ( not [x,y] in R2 or [x,y] in R1 ) )
 ( [x,y] in R1 iff for A being Subset of T st A is open holds
( x in A iff y in A ) ) by A11;
hence  ( ( not [x,y] in R1 or [x,y] in R2 ) & ( not [x,y] in R2 or [x,y] in R1 ) ) by A12; ::_thesis: verum
end;
end;

:: deftheorem Def3 defines Indiscernibility T_0TOPSP:def_3_:_
 for T being non empty TopStruct
for b2 being Equivalence_Relation of the carrier of T holds
( b2 = Indiscernibility T iff for p, q being Point of T holds
( [p,q] in b2 iff for A being Subset of T st A is open holds
( p in A iff q in A ) ) );

definition
let T be non empty TopStruct ;
func Indiscernible T ->  non empty a_partition of the carrier of T equals :: T_0TOPSP:def 4
 Class (Indiscernibility T);
coherence
 Class (Indiscernibility T) is non empty a_partition of the carrier of T ;
end;

:: deftheorem  defines Indiscernible T_0TOPSP:def_4_:_
 for T being non empty TopStruct holds Indiscernible T = Class (Indiscernibility T);

definition
let T be non empty TopSpace;
func T_0-reflex T ->  TopSpace equals :: T_0TOPSP:def 5
 space (Indiscernible T);
correctness
coherence
space (Indiscernible T) is TopSpace;
;
end;

:: deftheorem  defines T_0-reflex T_0TOPSP:def_5_:_
 for T being non empty TopSpace holds T_0-reflex T = space (Indiscernible T);

registration
let T be non empty TopSpace;
cluster T_0-reflex T ->  non empty ;
coherence
 not T_0-reflex T is empty ;
end;

definition
let T be non empty TopSpace;
func T_0-canonical_map T ->  continuous Function of T,(T_0-reflex T) equals :: T_0TOPSP:def 6
 Proj (Indiscernible T);
coherence
 Proj (Indiscernible T) is continuous Function of T,(T_0-reflex T) ;
end;

:: deftheorem  defines T_0-canonical_map T_0TOPSP:def_6_:_
 for T being non empty TopSpace holds T_0-canonical_map T = Proj (Indiscernible T);

theorem Th2: :: T_0TOPSP:2
for T being non empty TopSpace
for V being Subset of (T_0-reflex T) holds
( V is open iff union V in the topology of T )
proof
let T be non empty TopSpace; ::_thesis: for V being Subset of (T_0-reflex T) holds
( V is open iff union V in the topology of T )
let V be Subset of (T_0-reflex T); ::_thesis: ( V is open iff union V in the topology of T )
A1: V is Subset of (Indiscernible T) by BORSUK_1:def_7;
hereby  ::_thesis: ( union V in the topology of T implies V is open )
assume  V is open ; ::_thesis: union V in the topology of T
then  V in the topology of (T_0-reflex T) by PRE_TOPC:def_2;
hence  union V in the topology of T by A1, BORSUK_1:27; ::_thesis: verum
end;
assume  union V in the topology of T ; ::_thesis: V is open
then  V in the topology of (space (Indiscernible T)) by A1, BORSUK_1:27;
hence  V is open by PRE_TOPC:def_2; ::_thesis: verum
end;

theorem Th3: :: T_0TOPSP:3
for T being non empty TopSpace
for C being set holds
( C is Point of (T_0-reflex T) iff ex p being Point of T st C = Class ((Indiscernibility T),p) )
proof
let T be non empty TopSpace; ::_thesis: for C being set holds
( C is Point of (T_0-reflex T) iff ex p being Point of T st C = Class ((Indiscernibility T),p) )
set TR = T_0-reflex T;
set R = Indiscernibility T;
let C be set ; ::_thesis: ( C is Point of (T_0-reflex T) iff ex p being Point of T st C = Class ((Indiscernibility T),p) )
hereby  ::_thesis: ( ex p being Point of T st C = Class ((Indiscernibility T),p) implies C is Point of (T_0-reflex T) )
assume  C is Point of (T_0-reflex T) ; ::_thesis: ex p being Point of T st C = Class ((Indiscernibility T),p)
then  C in the carrier of (T_0-reflex T) ;
then  C in Indiscernible T by BORSUK_1:def_7;
hence  ex p being Point of T st C = Class ((Indiscernibility T),p) by EQREL_1:36; ::_thesis: verum
end;
assume  ex p being Point of T st C = Class ((Indiscernibility T),p) ; ::_thesis: C is Point of (T_0-reflex T)
then  C in Class (Indiscernibility T) by EQREL_1:def_3;
hence  C is Point of (T_0-reflex T) by BORSUK_1:def_7; ::_thesis: verum
end;

theorem Th4: :: T_0TOPSP:4
for T being non empty TopSpace
for p being Point of T holds (T_0-canonical_map T) . p = Class ((Indiscernibility T),p)
proof
let T be non empty TopSpace; ::_thesis: for p being Point of T holds (T_0-canonical_map T) . p = Class ((Indiscernibility T),p)
let p be Point of T; ::_thesis: (T_0-canonical_map T) . p = Class ((Indiscernibility T),p)
set F = T_0-canonical_map T;
set R = Indiscernibility T;
 (T_0-canonical_map T) . p in the carrier of (T_0-reflex T) ;
then  (T_0-canonical_map T) . p in Indiscernible T by BORSUK_1:def_7;
then consider y being Element of T such that
A1: (T_0-canonical_map T) . p = Class ((Indiscernibility T),y) by EQREL_1:36;
 p in Class ((Indiscernibility T),y) by A1, BORSUK_1:28;
hence  (T_0-canonical_map T) . p = Class ((Indiscernibility T),p) by A1, EQREL_1:23; ::_thesis: verum
end;

theorem Th5: :: T_0TOPSP:5
for T being non empty TopSpace
for p, q being Point of T holds
( (T_0-canonical_map T) . q = (T_0-canonical_map T) . p iff [q,p] in Indiscernibility T )
proof
let T be non empty TopSpace; ::_thesis: for p, q being Point of T holds
( (T_0-canonical_map T) . q = (T_0-canonical_map T) . p iff [q,p] in Indiscernibility T )
let p, q be Point of T; ::_thesis: ( (T_0-canonical_map T) . q = (T_0-canonical_map T) . p iff [q,p] in Indiscernibility T )
set F = T_0-canonical_map T;
set R = Indiscernibility T;
hereby  ::_thesis: ( [q,p] in Indiscernibility T implies (T_0-canonical_map T) . q = (T_0-canonical_map T) . p )
assume  (T_0-canonical_map T) . q = (T_0-canonical_map T) . p ; ::_thesis: [q,p] in Indiscernibility T
then  q in (T_0-canonical_map T) . p by BORSUK_1:28;
then  q in Class ((Indiscernibility T),p) by Th4;
hence  [q,p] in Indiscernibility T by EQREL_1:19; ::_thesis: verum
end;
assume  [q,p] in Indiscernibility T ; ::_thesis: (T_0-canonical_map T) . q = (T_0-canonical_map T) . p
then  Class ((Indiscernibility T),q) = Class ((Indiscernibility T),p) by EQREL_1:35;
then  (T_0-canonical_map T) . q = Class ((Indiscernibility T),p) by Th4;
hence  (T_0-canonical_map T) . q = (T_0-canonical_map T) . p by Th4; ::_thesis: verum
end;

theorem Th6: :: T_0TOPSP:6
for T being non empty TopSpace
for A being Subset of T st A is open holds
for p, q being Point of T st p in A & (T_0-canonical_map T) . p = (T_0-canonical_map T) . q holds
q in A
proof
let T be non empty TopSpace; ::_thesis: for A being Subset of T st A is open holds
for p, q being Point of T st p in A & (T_0-canonical_map T) . p = (T_0-canonical_map T) . q holds
q in A
let A be Subset of T; ::_thesis: ( A is open implies for p, q being Point of T st p in A & (T_0-canonical_map T) . p = (T_0-canonical_map T) . q holds
q in A )
assume A1: A is open ; ::_thesis: for p, q being Point of T st p in A & (T_0-canonical_map T) . p = (T_0-canonical_map T) . q holds
q in A
set F = T_0-canonical_map T;
let p, q be Point of T; ::_thesis: ( p in A & (T_0-canonical_map T) . p = (T_0-canonical_map T) . q implies q in A )
assume that
A2: p in A and
A3: (T_0-canonical_map T) . p = (T_0-canonical_map T) . q ; ::_thesis: q in A
A4: (T_0-canonical_map T) . p = Class ((Indiscernibility T),p) by Th4;
 q in (T_0-canonical_map T) . p by A3, BORSUK_1:28;
then  [q,p] in Indiscernibility T by A4, EQREL_1:19;
hence  q in A by A1, A2, Def3; ::_thesis: verum
end;

theorem Th7: :: T_0TOPSP:7
for T being non empty TopSpace
for A being Subset of T st A is open holds
for C being Subset of T st C in Indiscernible T & C meets A holds
C c= A
proof
let T be non empty TopSpace; ::_thesis: for A being Subset of T st A is open holds
for C being Subset of T st C in Indiscernible T & C meets A holds
C c= A
let A be Subset of T; ::_thesis: ( A is open implies for C being Subset of T st C in Indiscernible T & C meets A holds
C c= A )
assume A1: A is open ; ::_thesis: for C being Subset of T st C in Indiscernible T & C meets A holds
C c= A
set R = Indiscernibility T;
let C be Subset of T; ::_thesis: ( C in Indiscernible T & C meets A implies C c= A )
assume that
A2: C in Indiscernible T and
A3: C meets A ; ::_thesis: C c= A
consider y being set  such that
A4: y in C and
A5: y in A by A3, XBOOLE_0:3;
consider x being set  such that
 x in the carrier of T and
A6: C = Class ((Indiscernibility T),x) by A2, EQREL_1:def_3;
 for p being set st p in C holds
p in A
proof
let p be set ; ::_thesis: ( p in C implies p in A )
 [y,x] in Indiscernibility T by A6, A4, EQREL_1:19;
then A7: [x,y] in Indiscernibility T by EQREL_1:6;
assume A8: p in C ; ::_thesis: p in A
then  [p,x] in Indiscernibility T by A6, EQREL_1:19;
then  [p,y] in Indiscernibility T by A7, EQREL_1:7;
hence  p in A by A1, A5, A8, Def3; ::_thesis: verum
end;
hence  C c= A by TARSKI:def_3; ::_thesis: verum
end;

theorem Th8: :: T_0TOPSP:8
for T being non empty TopSpace holds T_0-canonical_map T is open
proof
let T be non empty TopSpace; ::_thesis: T_0-canonical_map T is open
set F = T_0-canonical_map T;
 for A being Subset of T st A is open holds
(T_0-canonical_map T) .: A is open
proof
set D = Indiscernible T;
A1: T_0-canonical_map T = proj (Indiscernible T) by BORSUK_1:def_8;
let A be Subset of T; ::_thesis: ( A is open implies (T_0-canonical_map T) .: A is open )
assume A2: A is open ; ::_thesis: (T_0-canonical_map T) .: A is open
A3: for C being Subset of T st C in Indiscernible T & C meets A holds
C c= A by A2, Th7;
set A9 = (T_0-canonical_map T) .: A;
 (T_0-canonical_map T) .: A is Subset of (Indiscernible T) by BORSUK_1:def_7;
then  (T_0-canonical_map T) " ((T_0-canonical_map T) .: A) = union ((T_0-canonical_map T) .: A) by A1, EQREL_1:67;
then  A = union ((T_0-canonical_map T) .: A) by A1, A3, EQREL_1:69;
then  union ((T_0-canonical_map T) .: A) in the topology of T by A2, PRE_TOPC:def_2;
hence  (T_0-canonical_map T) .: A is open by Th2; ::_thesis: verum
end;
hence  T_0-canonical_map T is open by Def2; ::_thesis: verum
end;

Lm1:  for T being non empty TopSpace
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 ) ) )
proof
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, Def2;
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 set 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 set 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
end;

definition
let T be TopStruct ;
redefine attr T is T_0  means :Def7: :: T_0TOPSP:def 7
( T is empty or for x, y being Point of T st x <> y holds
ex V being Subset of T st
( V is open & ( ( x in V & not y in V ) or ( y in V & not x in V ) ) ) );
compatibility
 ( T is T_0 iff ( T is empty or for x, y being Point of T st x <> y holds
ex V being Subset of T st
( V is open & ( ( x in V & not y in V ) or ( y in V & not x in V ) ) ) ) )
proof
thus  ( not T is T_0 or T is empty or for x, y being Point of T st x <> y holds
ex V being Subset of T st
( V is open & ( ( x in V & not y in V ) or ( y in V & not x in V ) ) ) ) by PRE_TOPC:def_8; ::_thesis: ( ( T is empty or for x, y being Point of T st x <> y holds
ex V being Subset of T st
( V is open & ( ( x in V & not y in V ) or ( y in V & not x in V ) ) ) ) implies T is T_0 )
assume A1: ( T is empty or for x, y being Point of T st x <> y holds
ex V being Subset of T st
( V is open & ( ( x in V & not y in V ) or ( y in V & not x in V ) ) ) ) ; ::_thesis: T is T_0
let x, y be Point of T; :: according to PRE_TOPC:def_8 ::_thesis: ( ex b1 being Element of K10( the carrier of T) st
( b1 is open & ( ( x in b1 & not y in b1 ) or ( y in b1 & not x in b1 ) ) ) or x = y )
assume A2: for G being Subset of T st G is open holds
( x in G iff y in G ) ; ::_thesis: x = y
percases ( T is empty or for x, y being Point of T st x <> y holds
ex V being Subset of T st
( V is open & ( ( x in V & not y in V ) or ( y in V & not x in V ) ) ) ) by A1;
supposeA3: T is empty ; ::_thesis: x = y
then  x = {} by SUBSET_1:def_1;
hence  x = y by A3, SUBSET_1:def_1; ::_thesis: verum
end;
suppose for x, y being Point of T st x <> y holds
ex V being Subset of T st
( V is open & ( ( x in V & not y in V ) or ( y in V & not x in V ) ) ) ; ::_thesis: x = y
hence  x = y by A2; ::_thesis: verum
end;
end;
end;
end;

:: deftheorem Def7 defines T_0 T_0TOPSP:def_7_:_
 for T being TopStruct holds
( T is T_0 iff ( T is empty or for x, y being Point of T st x <> y holds
ex V being Subset of T st
( V is open & ( ( x in V & not y in V ) or ( y in V & not x in V ) ) ) ) );

registration
cluster non empty TopSpace-like T_0 for TopStruct ;
existence
 ex b1 being TopSpace st
( b1 is T_0 & not b1 is empty )
proof
set T = the non empty TopSpace;
take  T_0-reflex the non empty TopSpace ; ::_thesis: ( T_0-reflex the non empty TopSpace is T_0 & not T_0-reflex the non empty TopSpace is empty )
 for x, y being Point of (T_0-reflex the non empty TopSpace) st x <> y holds
ex V being Subset of (T_0-reflex the non empty TopSpace) st
( V is open & ( ( x in V & not y in V ) or ( y in V & not x in V ) ) ) by Lm1;
hence  ( T_0-reflex the non empty TopSpace is T_0 & not T_0-reflex the non empty TopSpace is empty ) by Def7; ::_thesis: verum
end;
end;

definition
mode T_0-TopSpace is non empty T_0 TopSpace;
end;

theorem :: T_0TOPSP:9
for T being non empty TopSpace holds T_0-reflex T is T_0-TopSpace
proof
let T be non empty TopSpace; ::_thesis: T_0-reflex T is T_0-TopSpace
 for x, y being Point of (T_0-reflex T) st not x = y holds
ex A being Subset of (T_0-reflex T) st
( A is open & ( ( x in A & not y in A ) or ( y in A & not x in A ) ) ) by Lm1;
hence  T_0-reflex T is T_0-TopSpace by Def7; ::_thesis: verum
end;

theorem :: T_0TOPSP:10
for T, S being non empty TopSpace st ex h being Function of (T_0-reflex S),(T_0-reflex T) st
( h is being_homeomorphism & T_0-canonical_map T,h * (T_0-canonical_map S) are_fiberwise_equipotent ) holds
T,S are_homeomorphic
proof
let T, S be non empty TopSpace; ::_thesis: ( ex h being Function of (T_0-reflex S),(T_0-reflex T) st
( h is being_homeomorphism & T_0-canonical_map T,h * (T_0-canonical_map S) are_fiberwise_equipotent ) implies T,S are_homeomorphic )
set F = T_0-canonical_map T;
set G = T_0-canonical_map S;
set TR = T_0-reflex T;
set SR = T_0-reflex S;
given h being Function of (T_0-reflex S),(T_0-reflex T) such that A1: h is being_homeomorphism and
A2: T_0-canonical_map T,h * (T_0-canonical_map S) are_fiberwise_equipotent ; ::_thesis: T,S are_homeomorphic
consider f being Function such that
A3: dom f = dom (T_0-canonical_map T) and
A4: rng f = dom (h * (T_0-canonical_map S)) and
A5: f is one-to-one and
A6: T_0-canonical_map T = (h * (T_0-canonical_map S)) * f by A2, CLASSES1:77;
A7: dom f = the carrier of T by A3, FUNCT_2:def_1;
A8: h is continuous by A1, TOPS_2:def_5;
A9: h is one-to-one by A1, TOPS_2:def_5;
reconsider f = f as Function of T,S by A4, A7, FUNCT_2:def_1, RELSET_1:4;
take  f ; :: according to T_0TOPSP:def_1 ::_thesis: f is being_homeomorphism
thus A10: ( dom f = [#] T & rng f = [#] S ) by A4, FUNCT_2:def_1; :: according to TOPS_2:def_5 ::_thesis: ( f is one-to-one & f is continuous & f " is continuous )
A11: rng h = [#] (T_0-reflex T) by A1, TOPS_2:def_5;
A12: [#] (T_0-reflex S) <> {} ;
A13: for A being Subset of S st A is open holds
f " A is open
proof
set g = h * (T_0-canonical_map S);
let A be Subset of S; ::_thesis: ( A is open implies f " A is open )
set B = (h * (T_0-canonical_map S)) .: A;
A14: h " is continuous by A1, TOPS_2:def_5;
assume A15: A is open ; ::_thesis: f " A is open
A16: for x1, x2 being Element of S st x1 in A & (h * (T_0-canonical_map S)) . x1 = (h * (T_0-canonical_map S)) . x2 holds
x2 in A
proof
let x1, x2 be Element of S; ::_thesis: ( x1 in A & (h * (T_0-canonical_map S)) . x1 = (h * (T_0-canonical_map S)) . x2 implies x2 in A )
assume that
A17: x1 in A and
A18: (h * (T_0-canonical_map S)) . x1 = (h * (T_0-canonical_map S)) . x2 ; ::_thesis: x2 in A
 h . ((T_0-canonical_map S) . x1) = (h * (T_0-canonical_map S)) . x2 by A18, FUNCT_2:15;
then  h . ((T_0-canonical_map S) . x1) = h . ((T_0-canonical_map S) . x2) by FUNCT_2:15;
then  (T_0-canonical_map S) . x1 = (T_0-canonical_map S) . x2 by A9, FUNCT_2:19;
hence  x2 in A by A15, A17, Th6; ::_thesis: verum
end;
 T_0-canonical_map S is open by Th8;
then  (T_0-canonical_map S) .: A is open by A15, Def2;
then A19: (h ") " ((T_0-canonical_map S) .: A) is open by A12, A14, TOPS_2:43;
A20: h is onto by A11, FUNCT_2:def_3;
 h .: ((T_0-canonical_map S) .: A) = (h ") " ((T_0-canonical_map S) .: A) by A9, FUNCT_1:84;
then  h .: ((T_0-canonical_map S) .: A) is open by A9, A19, A20, TOPS_2:def_4;
then A21: (h * (T_0-canonical_map S)) .: A is open by RELAT_1:126;
 [#] (T_0-reflex T) <> {} ;
then A22: (T_0-canonical_map T) " ((h * (T_0-canonical_map S)) .: A) is open by A21, TOPS_2:43;
 (T_0-canonical_map T) " ((h * (T_0-canonical_map S)) .: A) = f " ((h * (T_0-canonical_map S)) " ((h * (T_0-canonical_map S)) .: A)) by A6, RELAT_1:146;
hence  f " A is open by A22, A16, Th1; ::_thesis: verum
end;
A23: dom h = [#] (T_0-reflex S) by A1, TOPS_2:def_5;
A24: for A being Subset of T st A is open holds
(f ") " A is open
proof
set g = (h ") * (T_0-canonical_map T);
let A be Subset of T; ::_thesis: ( A is open implies (f ") " A is open )
set B = ((h ") * (T_0-canonical_map T)) .: A;
assume A25: A is open ; ::_thesis: (f ") " A is open
A26: for x1, x2 being Element of T st x1 in A & ((h ") * (T_0-canonical_map T)) . x1 = ((h ") * (T_0-canonical_map T)) . x2 holds
x2 in A
proof
let x1, x2 be Element of T; ::_thesis: ( x1 in A & ((h ") * (T_0-canonical_map T)) . x1 = ((h ") * (T_0-canonical_map T)) . x2 implies x2 in A )
assume that
A27: x1 in A and
A28: ((h ") * (T_0-canonical_map T)) . x1 = ((h ") * (T_0-canonical_map T)) . x2 ; ::_thesis: x2 in A
 (h ") . ((T_0-canonical_map T) . x1) = ((h ") * (T_0-canonical_map T)) . x2 by A28, FUNCT_2:15;
then A29: (h ") . ((T_0-canonical_map T) . x1) = (h ") . ((T_0-canonical_map T) . x2) by FUNCT_2:15;
 h " is one-to-one by A11, A9, TOPS_2:50;
then  (T_0-canonical_map T) . x1 = (T_0-canonical_map T) . x2 by A29, FUNCT_2:19;
hence  x2 in A by A25, A27, Th6; ::_thesis: verum
end;
 T_0-canonical_map T = h * ((T_0-canonical_map S) * f) by A6, RELAT_1:36;
then  (h ") * (T_0-canonical_map T) = ((h ") * h) * ((T_0-canonical_map S) * f) by RELAT_1:36;
then  (h ") * (T_0-canonical_map T) = (id the carrier of (T_0-reflex S)) * ((T_0-canonical_map S) * f) by A23, A11, A9, TOPS_2:52;
then  ((h ") * (T_0-canonical_map T)) * (f ") = ((T_0-canonical_map S) * f) * (f ") by FUNCT_2:17;
then  ((h ") * (T_0-canonical_map T)) * (f ") = (T_0-canonical_map S) * (f * (f ")) by RELAT_1:36;
then  ((h ") * (T_0-canonical_map T)) * (f ") = (T_0-canonical_map S) * (id the carrier of S) by A5, A10, TOPS_2:52;
then  T_0-canonical_map S = ((h ") * (T_0-canonical_map T)) * (f ") by FUNCT_2:17;
then A30: (T_0-canonical_map S) " (((h ") * (T_0-canonical_map T)) .: A) = (f ") " (((h ") * (T_0-canonical_map T)) " (((h ") * (T_0-canonical_map T)) .: A)) by RELAT_1:146;
 T_0-canonical_map T is open by Th8;
then  (T_0-canonical_map T) .: A is open by A25, Def2;
then A31: h " ((T_0-canonical_map T) .: A) is open by A11, A8, TOPS_2:43;
 ((h ") * (T_0-canonical_map T)) .: A = (h ") .: ((T_0-canonical_map T) .: A) by RELAT_1:126;
then  (T_0-canonical_map S) " (((h ") * (T_0-canonical_map T)) .: A) = (T_0-canonical_map S) " (h " ((T_0-canonical_map T) .: A)) by A11, A9, TOPS_2:55;
then  (T_0-canonical_map S) " (((h ") * (T_0-canonical_map T)) .: A) is open by A12, A31, TOPS_2:43;
hence  (f ") " A is open by A26, A30, Th1; ::_thesis: verum
end;
thus  f is one-to-one by A5; ::_thesis: ( f is continuous & f " is continuous )
 [#] S <> {} ;
hence  f is continuous by A13, TOPS_2:43; ::_thesis: f " is continuous
 [#] T <> {} ;
hence  f " is continuous by A24, TOPS_2:43; ::_thesis: verum
end;

theorem Th11: :: T_0TOPSP:11
for T being non empty TopSpace
for T0 being T_0-TopSpace
for f being continuous Function of T,T0
for p, q being Point of T st [p,q] in Indiscernibility T holds
f . p = f . q
proof
let T be non empty TopSpace; ::_thesis: for T0 being T_0-TopSpace
for f being continuous Function of T,T0
for p, q being Point of T st [p,q] in Indiscernibility T holds
f . p = f . q
let T0 be T_0-TopSpace; ::_thesis: for f being continuous Function of T,T0
for p, q being Point of T st [p,q] in Indiscernibility T holds
f . p = f . q
let f be continuous Function of T,T0; ::_thesis: for p, q being Point of T st [p,q] in Indiscernibility T holds
f . p = f . q
let p, q be Point of T; ::_thesis: ( [p,q] in Indiscernibility T implies f . p = f . q )
set p9 = f . p;
set q9 = f . q;
assume that
A1: [p,q] in Indiscernibility T and
A2: not f . p = f . q ; ::_thesis: contradiction
consider V being Subset of T0 such that
A3: V is open and
A4: ( ( f . p in V & not f . q in V ) or ( f . q in V & not f . p in V ) ) by A2, Def7;
set A = f " V;
 [#] T0 <> {} ;
then A5: f " V is open by A3, TOPS_2:43;
reconsider f = f as Function of the carrier of T, the carrier of T0 ;
 q in the carrier of T ;
then A6: q in dom f by FUNCT_2:def_1;
 p in the carrier of T ;
then  p in dom f by FUNCT_2:def_1;
then  ( ( p in f " V & not q in f " V ) or ( q in f " V & not p in f " V ) ) by A4, A6, FUNCT_1:def_7;
hence  contradiction by A1, A5, Def3; ::_thesis: verum
end;

theorem Th12: :: T_0TOPSP:12
for T being non empty TopSpace
for T0 being T_0-TopSpace
for f being continuous Function of T,T0
for p being Point of T holds f .: (Class ((Indiscernibility T),p)) = {(f . p)}
proof
let T be non empty TopSpace; ::_thesis: for T0 being T_0-TopSpace
for f being continuous Function of T,T0
for p being Point of T holds f .: (Class ((Indiscernibility T),p)) = {(f . p)}
let T0 be T_0-TopSpace; ::_thesis: for f being continuous Function of T,T0
for p being Point of T holds f .: (Class ((Indiscernibility T),p)) = {(f . p)}
let f be continuous Function of T,T0; ::_thesis: for p being Point of T holds f .: (Class ((Indiscernibility T),p)) = {(f . p)}
let p be Point of T; ::_thesis: f .: (Class ((Indiscernibility T),p)) = {(f . p)}
set R = Indiscernibility T;
 for y being set holds
( y in f .: (Class ((Indiscernibility T),p)) iff y in {(f . p)} )
proof
let y be set ; ::_thesis: ( y in f .: (Class ((Indiscernibility T),p)) iff y in {(f . p)} )
hereby  ::_thesis: ( y in {(f . p)} implies y in f .: (Class ((Indiscernibility T),p)) )
assume  y in f .: (Class ((Indiscernibility T),p)) ; ::_thesis: y in {(f . p)}
then consider x being set  such that
A1: x in the carrier of T and
A2: x in Class ((Indiscernibility T),p) and
A3: y = f . x by FUNCT_2:64;
 [x,p] in Indiscernibility T by A2, EQREL_1:19;
then  f . x = f . p by A1, Th11;
hence  y in {(f . p)} by A3, TARSKI:def_1; ::_thesis: verum
end;
assume  y in {(f . p)} ; ::_thesis: y in f .: (Class ((Indiscernibility T),p))
then A4: y = f . p by TARSKI:def_1;
 p in Class ((Indiscernibility T),p) by EQREL_1:20;
hence  y in f .: (Class ((Indiscernibility T),p)) by A4, FUNCT_2:35; ::_thesis: verum
end;
hence  f .: (Class ((Indiscernibility T),p)) = {(f . p)} by TARSKI:1; ::_thesis: verum
end;

theorem :: T_0TOPSP:13
for T being non empty TopSpace
for T0 being T_0-TopSpace
for f being continuous Function of T,T0 ex h being continuous Function of (T_0-reflex T),T0 st f = h * (T_0-canonical_map T)
proof
let T be non empty TopSpace; ::_thesis: for T0 being T_0-TopSpace
for f being continuous Function of T,T0 ex h being continuous Function of (T_0-reflex T),T0 st f = h * (T_0-canonical_map T)
let T0 be T_0-TopSpace; ::_thesis: for f being continuous Function of T,T0 ex h being continuous Function of (T_0-reflex T),T0 st f = h * (T_0-canonical_map T)
let f be continuous Function of T,T0; ::_thesis: ex h being continuous Function of (T_0-reflex T),T0 st f = h * (T_0-canonical_map T)
set F = T_0-canonical_map T;
set R = Indiscernibility T;
set TR = T_0-reflex T;
defpred S1[ set , set ] means $2 in f .: $1;
A1: for C being set st C in the carrier of (T_0-reflex T) holds
ex y being set st
( y in the carrier of T0 & S1[C,y] )
proof
let C be set ; ::_thesis: ( C in the carrier of (T_0-reflex T) implies ex y being set st
( y in the carrier of T0 & S1[C,y] ) )
assume  C in the carrier of (T_0-reflex T) ; ::_thesis: ex y being set st
( y in the carrier of T0 & S1[C,y] )
then consider p being Point of T such that
A2: C = Class ((Indiscernibility T),p) by Th3;
A3: f . p in {(f . p)} by TARSKI:def_1;
 f .: C = {(f . p)} by A2, Th12;
hence  ex y being set st
( y in the carrier of T0 & S1[C,y] ) by A3; ::_thesis: verum
end;
 ex h being Function of the carrier of (T_0-reflex T), the carrier of T0 st
for C being set st C in the carrier of (T_0-reflex T) holds
S1[C,h . C] from FUNCT_2:sch_1(A1);
then consider h being Function of the carrier of (T_0-reflex T), the carrier of T0 such that
A4: for C being set st C in the carrier of (T_0-reflex T) holds
h . C in f .: C ;
A5: for p being Point of T holds h . (Class ((Indiscernibility T),p)) = f . p
proof
let p be Point of T; ::_thesis: h . (Class ((Indiscernibility T),p)) = f . p
 Class ((Indiscernibility T),p) is Point of (T_0-reflex T) by Th3;
then  h . (Class ((Indiscernibility T),p)) in f .: (Class ((Indiscernibility T),p)) by A4;
then  h . (Class ((Indiscernibility T),p)) in {(f . p)} by Th12;
hence  h . (Class ((Indiscernibility T),p)) = f . p by TARSKI:def_1; ::_thesis: verum
end;
reconsider h = h as Function of (T_0-reflex T),T0 ;
A6: [#] T0 <> {} ;
 for W being Subset of T0 st W is open holds
h " W is open
proof
let W be Subset of T0; ::_thesis: ( W is open implies h " W is open )
assume  W is open ; ::_thesis: h " W is open
then A7: f " W is open by A6, TOPS_2:43;
set V = h " W;
 for x being set holds
( x in union (h " W) iff x in f " W )
proof
let x be set ; ::_thesis: ( x in union (h " W) iff x in f " W )
hereby  ::_thesis: ( x in f " W implies x in union (h " W) )
assume  x in union (h " W) ; ::_thesis: x in f " W
then consider C being set  such that
A8: x in C and
A9: C in h " W by TARSKI:def_4;
consider p being Point of T such that
A10: C = Class ((Indiscernibility T),p) by A9, Th3;
 x in the carrier of T by A8, A10;
then A11: x in dom f by FUNCT_2:def_1;
 [x,p] in Indiscernibility T by A8, A10, EQREL_1:19;
then A12: C = Class ((Indiscernibility T),x) by A8, A10, EQREL_1:35;
 h . C in W by A9, FUNCT_1:def_7;
then  f . x in W by A5, A8, A12;
hence  x in f " W by A11, FUNCT_1:def_7; ::_thesis: verum
end;
assume A13: x in f " W ; ::_thesis: x in union (h " W)
then  f . x in W by FUNCT_1:def_7;
then A14: h . (Class ((Indiscernibility T),x)) in W by A5, A13;
 Class ((Indiscernibility T),x) is Point of (T_0-reflex T) by A13, Th3;
then A15: Class ((Indiscernibility T),x) in h " W by A14, FUNCT_2:38;
 x in Class ((Indiscernibility T),x) by A13, EQREL_1:20;
hence  x in union (h " W) by A15, TARSKI:def_4; ::_thesis: verum
end;
then  union (h " W) = f " W by TARSKI:1;
then  union (h " W) in the topology of T by A7, PRE_TOPC:def_2;
hence  h " W is open by Th2; ::_thesis: verum
end;
then reconsider h = h as continuous Function of (T_0-reflex T),T0 by A6, TOPS_2:43;
set H = h * (T_0-canonical_map T);
 for x being set st x in the carrier of T holds
f . x = (h * (T_0-canonical_map T)) . x
proof
let x be set ; ::_thesis: ( x in the carrier of T implies f . x = (h * (T_0-canonical_map T)) . x )
assume A16: x in the carrier of T ; ::_thesis: f . x = (h * (T_0-canonical_map T)) . x
then  Class ((Indiscernibility T),x) in Class (Indiscernibility T) by EQREL_1:def_3;
then A17: Class ((Indiscernibility T),x) in the carrier of (T_0-reflex T) by BORSUK_1:def_7;
 ( x in dom (T_0-canonical_map T) & (T_0-canonical_map T) . x = Class ((Indiscernibility T),x) ) by A16, Th4, FUNCT_2:def_1;
then  (h * (T_0-canonical_map T)) . x = h . (Class ((Indiscernibility T),x)) by FUNCT_1:13;
then  (h * (T_0-canonical_map T)) . x in f .: (Class ((Indiscernibility T),x)) by A4, A17;
then  (h * (T_0-canonical_map T)) . x in {(f . x)} by A16, Th12;
hence  f . x = (h * (T_0-canonical_map T)) . x by TARSKI:def_1; ::_thesis: verum
end;
hence  ex h being continuous Function of (T_0-reflex T),T0 st f = h * (T_0-canonical_map T) by FUNCT_2:12; ::_thesis: verum
end;