:: BORSUK_1 semantic presentation

begin


theorem Th1: :: BORSUK_1:1
for X being TopStruct
for Y being SubSpace of X holds the carrier of Y c= the carrier of X
proof
let X be TopStruct ; ::_thesis: for Y being SubSpace of X holds the carrier of Y c= the carrier of X
let Y be SubSpace of X; ::_thesis: the carrier of Y c= the carrier of X
 ( the carrier of Y = [#] Y & the carrier of X = [#] X ) ;
hence  the carrier of Y c= the carrier of X by PRE_TOPC:def_4; ::_thesis: verum
end;

definition
let X, Y be non empty TopSpace;
let F be Function of X,Y;
redefine attr F is continuous  means :: BORSUK_1:def 1
 for W being Point of X
for G being a_neighborhood of F . W ex H being a_neighborhood of W st F .: H c= G;
compatibility
 ( F is continuous iff for W being Point of X
for G being a_neighborhood of F . W ex H being a_neighborhood of W st F .: H c= G )
proof
A1: [#] Y <> {} ;
thus  ( F is continuous implies for W being Point of X
for G being a_neighborhood of F . W ex H being a_neighborhood of W st F .: H c= G ) ::_thesis: ( ( for W being Point of X
for G being a_neighborhood of F . W ex H being a_neighborhood of W st F .: H c= G ) implies F is continuous )
proof
assume A2: F is continuous ; ::_thesis: for W being Point of X
for G being a_neighborhood of F . W ex H being a_neighborhood of W st F .: H c= G
let W be Point of X; ::_thesis: for G being a_neighborhood of F . W ex H being a_neighborhood of W st F .: H c= G
let G be a_neighborhood of F . W; ::_thesis: ex H being a_neighborhood of W st F .: H c= G
 F . W in Int G by CONNSP_2:def_1;
then A3: W in F " (Int G) by FUNCT_2:38;
 F " (Int G) is open by A1, A2, TOPS_2:43;
then  W in Int (F " (Int G)) by A3, TOPS_1:23;
then reconsider H = F " (Int G) as a_neighborhood of W by CONNSP_2:def_1;
take  H ; ::_thesis: F .: H c= G
 H c= F " G by RELAT_1:143, TOPS_1:16;
hence  F .: H c= G by EQREL_1:46; ::_thesis: verum
end;
assume A4: for W being Point of X
for G being a_neighborhood of F . W ex H being a_neighborhood of W st F .: H c= G ; ::_thesis: F is continuous
now__::_thesis:_for_P1_being_Subset_of_Y_st_P1_is_open_holds_
F_"_P1_is_open
let P1 be Subset of Y; ::_thesis: ( P1 is open implies F " P1 is open )
assume A5: P1 is open ; ::_thesis: F " P1 is open
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_F_"_P1_implies_ex_P_being_Subset_of_X_st_
(_P_is_open_&_P_c=_F_"_P1_&_x_in_P_)_)_&_(_ex_P_being_Subset_of_X_st_
(_P_is_open_&_P_c=_F_"_P1_&_x_in_P_)_implies_x_in_F_"_P1_)_)
let x be set ; ::_thesis: ( ( x in F " P1 implies ex P being Subset of X st
( P is open & P c= F " P1 & x in P ) ) & ( ex P being Subset of X st
( P is open & P c= F " P1 & x in P ) implies x in F " P1 ) )
thus  ( x in F " P1 implies ex P being Subset of X st
( P is open & P c= F " P1 & x in P ) ) ::_thesis: ( ex P being Subset of X st
( P is open & P c= F " P1 & x in P ) implies x in F " P1 )
proof
assume A6: x in F " P1 ; ::_thesis: ex P being Subset of X st
( P is open & P c= F " P1 & x in P )
then reconsider W = x as Point of X ;
A7: Int P1 = P1 by A5, TOPS_1:23;
 F . W in P1 by A6, FUNCT_2:38;
then  P1 is a_neighborhood of F . W by A7, CONNSP_2:def_1;
then consider H being a_neighborhood of W such that
A8: F .: H c= P1 by A4;
take  Int H ; ::_thesis: ( Int H is open & Int H c= F " P1 & x in Int H )
thus  Int H is open ; ::_thesis: ( Int H c= F " P1 & x in Int H )
A9: Int H c= H by TOPS_1:16;
 dom F = the carrier of X by FUNCT_2:def_1;
then A10: H c= F " (F .: H) by FUNCT_1:76;
 F " (F .: H) c= F " P1 by A8, RELAT_1:143;
then  H c= F " P1 by A10, XBOOLE_1:1;
hence  Int H c= F " P1 by A9, XBOOLE_1:1; ::_thesis: x in Int H
thus  x in Int H by CONNSP_2:def_1; ::_thesis: verum
end;
thus  ( ex P being Subset of X st
( P is open & P c= F " P1 & x in P ) implies x in F " P1 ) ; ::_thesis: verum
end;
hence  F " P1 is open by TOPS_1:25; ::_thesis: verum
end;
hence  F is continuous by A1, TOPS_2:43; ::_thesis: verum
end;
end;

:: deftheorem  defines continuous BORSUK_1:def_1_:_
 for X, Y being non empty TopSpace
for F being Function of X,Y holds
( F is continuous iff for W being Point of X
for G being a_neighborhood of F . W ex H being a_neighborhood of W st F .: H c= G );


registration
let X, Y, Z be non empty TopSpace;
let F be continuous Function of X,Y;
let G be continuous Function of Y,Z;
clusterF * G ->  continuous for Function of X,Z;
coherence
 for b1 being Function of X,Z st b1 = G * F holds
b1 is continuous by TOPS_2:46;
end;

theorem Th2: :: BORSUK_1:2
for X, Y being non empty TopSpace
for A being continuous Function of X,Y
for G being Subset of Y holds A " (Int G) c= Int (A " G)
proof
let X, Y be non empty TopSpace; ::_thesis: for A being continuous Function of X,Y
for G being Subset of Y holds A " (Int G) c= Int (A " G)
let A be continuous Function of X,Y; ::_thesis: for G being Subset of Y holds A " (Int G) c= Int (A " G)
let G be Subset of Y; ::_thesis: A " (Int G) c= Int (A " G)
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in A " (Int G) or e in Int (A " G) )
A1: A " (Int G) c= A " G by RELAT_1:143, TOPS_1:16;
 [#] Y <> {} ;
then A2: A " (Int G) is open by TOPS_2:43;
assume  e in A " (Int G) ; ::_thesis: e in Int (A " G)
hence  e in Int (A " G) by A2, A1, TOPS_1:22; ::_thesis: verum
end;

theorem Th3: :: BORSUK_1:3
for Y, X being non empty TopSpace
for W being Point of Y
for A being continuous Function of X,Y
for G being a_neighborhood of W holds A " G is a_neighborhood of A " {W}
proof
let Y, X be non empty TopSpace; ::_thesis: for W being Point of Y
for A being continuous Function of X,Y
for G being a_neighborhood of W holds A " G is a_neighborhood of A " {W}
let W be Point of Y; ::_thesis: for A being continuous Function of X,Y
for G being a_neighborhood of W holds A " G is a_neighborhood of A " {W}
let A be continuous Function of X,Y; ::_thesis: for G being a_neighborhood of W holds A " G is a_neighborhood of A " {W}
let G be a_neighborhood of W; ::_thesis: A " G is a_neighborhood of A " {W}
 W in Int G by CONNSP_2:def_1;
then  {W} c= Int G by ZFMISC_1:31;
then A1: A " {W} c= A " (Int G) by RELAT_1:143;
 A " (Int G) c= Int (A " G) by Th2;
hence  A " {W} c= Int (A " G) by A1, XBOOLE_1:1; :: according to CONNSP_2:def_2 ::_thesis: verum
end;

definition
let X, Y be non empty TopSpace;
let W be Point of Y;
let A be continuous Function of X,Y;
let G be a_neighborhood of W;
:: original: "
redefine funcA " G ->  a_neighborhood of A " {W};
correctness
coherence
A " G is a_neighborhood of A " {W};
by Th3;
end;

theorem Th4: :: BORSUK_1:4
for X being non empty TopSpace
for A, B being Subset of X
for U being a_neighborhood of B st A c= B holds
U is a_neighborhood of A
proof
let X be non empty TopSpace; ::_thesis: for A, B being Subset of X
for U being a_neighborhood of B st A c= B holds
U is a_neighborhood of A
let A, B be Subset of X; ::_thesis: for U being a_neighborhood of B st A c= B holds
U is a_neighborhood of A
let U be a_neighborhood of B; ::_thesis: ( A c= B implies U is a_neighborhood of A )
assume A1: A c= B ; ::_thesis: U is a_neighborhood of A
 B c= Int U by CONNSP_2:def_2;
hence  A c= Int U by A1, XBOOLE_1:1; :: according to CONNSP_2:def_2 ::_thesis: verum
end;

registration
let X be non empty TopSpace;
let x be Point of X;
cluster{x} ->  compact for Subset of X;
coherence
 for b1 being Subset of X st b1 = {x} holds
b1 is compact
proof
reconsider B = {x} as Subset of X ;
now__::_thesis:_for_F_being_Subset-Family_of_X_st_F_is_Cover_of_B_&_F_is_open_holds_
ex_G_being_Subset-Family_of_X_st_
(_G_c=_F_&_G_is_Cover_of_B_&_G_is_finite_)
let F be Subset-Family of X; ::_thesis: ( F is Cover of B & F is open implies ex G being Subset-Family of X st
( G c= F & G is Cover of B & G is finite ) )
assume that
A1: F is Cover of B and
 F is open ; ::_thesis: ex G being Subset-Family of X st
( G c= F & G is Cover of B & G is finite )
 B c= union F by A1, SETFAM_1:def_11;
then  x in union F by ZFMISC_1:31;
then consider A being set  such that
A2: x in A and
A3: A in F by TARSKI:def_4;
reconsider G = {A} as Subset-Family of X by A3, ZFMISC_1:31;
take G = G; ::_thesis: ( G c= F & G is Cover of B & G is finite )
thus  G c= F by A3, ZFMISC_1:31; ::_thesis: ( G is Cover of B & G is finite )
 A in G by TARSKI:def_1;
then  x in union G by A2, TARSKI:def_4;
then  B c= union G by ZFMISC_1:31;
hence  G is Cover of B by SETFAM_1:def_11; ::_thesis: G is finite
thus  G is finite ; ::_thesis: verum
end;
hence  for b1 being Subset of X st b1 = {x} holds
b1 is compact by COMPTS_1:def_4; ::_thesis: verum
end;
end;

begin

definition
let X, Y be TopSpace;
func[:X,Y:] ->  strict TopSpace means :Def2: :: BORSUK_1:def 2
( the carrier of it = [: the carrier of X, the carrier of Y:] & the topology of it =  {  (union A) where A is Subset-Family of it : A c=  {  [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y )  }   }  );
existence
 ex b1 being strict TopSpace st
( the carrier of b1 = [: the carrier of X, the carrier of Y:] & the topology of b1 =  {  (union A) where A is Subset-Family of b1 : A c=  {  [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y )  }   }  )
proof
set t =  {  (union A) where A is Subset-Family of [: the carrier of X, the carrier of Y:] : A c=  {  [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y )  }   }  ;
  {  (union A) where A is Subset-Family of [: the carrier of X, the carrier of Y:] : A c=  {  [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y )  }   }  c= bool [: the carrier of X, the carrier of Y:]
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in  {  (union A) where A is Subset-Family of [: the carrier of X, the carrier of Y:] : A c=  {  [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y )  }   }  or e in bool [: the carrier of X, the carrier of Y:] )
assume  e in  {  (union A) where A is Subset-Family of [: the carrier of X, the carrier of Y:] : A c=  {  [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y )  }   }  ; ::_thesis: e in bool [: the carrier of X, the carrier of Y:]
then  ex A being Subset-Family of [: the carrier of X, the carrier of Y:] st
( e = union A & A c=  {  [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y )  }  ) ;
hence  e in bool [: the carrier of X, the carrier of Y:] ; ::_thesis: verum
end;
then reconsider t =  {  (union A) where A is Subset-Family of [: the carrier of X, the carrier of Y:] : A c=  {  [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y )  }   }  as Subset-Family of [: the carrier of X, the carrier of Y:] ;
set T = TopStruct(# [: the carrier of X, the carrier of Y:],t #);
now__::_thesis:_(_the_carrier_of_TopStruct(#_[:_the_carrier_of_X,_the_carrier_of_Y:],t_#)_in_the_topology_of_TopStruct(#_[:_the_carrier_of_X,_the_carrier_of_Y:],t_#)_&_(_for_a_being_Subset-Family_of_TopStruct(#_[:_the_carrier_of_X,_the_carrier_of_Y:],t_#)_st_a_c=_the_topology_of_TopStruct(#_[:_the_carrier_of_X,_the_carrier_of_Y:],t_#)_holds_
union_a_in_the_topology_of_TopStruct(#_[:_the_carrier_of_X,_the_carrier_of_Y:],t_#)_)_&_(_for_a,_b_being_Subset_of_TopStruct(#_[:_the_carrier_of_X,_the_carrier_of_Y:],t_#)_st_a_in_the_topology_of_TopStruct(#_[:_the_carrier_of_X,_the_carrier_of_Y:],t_#)_&_b_in_the_topology_of_TopStruct(#_[:_the_carrier_of_X,_the_carrier_of_Y:],t_#)_holds_
a_/\_b_in_the_topology_of_TopStruct(#_[:_the_carrier_of_X,_the_carrier_of_Y:],t_#)_)_)
reconsider A = {[: the carrier of X, the carrier of Y:]} as Subset-Family of [: the carrier of X, the carrier of Y:] by ZFMISC_1:68;
reconsider A = A as Subset-Family of [: the carrier of X, the carrier of Y:] ;
A1: A c=  {  [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y )  }
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in A or e in  {  [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y )  }  )
assume  e in A ; ::_thesis: e in  {  [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y )  }
then A2: e = [: the carrier of X, the carrier of Y:] by TARSKI:def_1;
 ( the carrier of X in the topology of X & the carrier of Y in the topology of Y ) by PRE_TOPC:def_1;
hence  e in  {  [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y )  }  by A2; ::_thesis: verum
end;
 the carrier of TopStruct(# [: the carrier of X, the carrier of Y:],t #) = union A by ZFMISC_1:25;
hence  the carrier of TopStruct(# [: the carrier of X, the carrier of Y:],t #) in the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #) by A1; ::_thesis: ( ( for a being Subset-Family of TopStruct(# [: the carrier of X, the carrier of Y:],t #) st a c= the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #) holds
union a in the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #) ) & ( for a, b being Subset of TopStruct(# [: the carrier of X, the carrier of Y:],t #) st a in the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #) & b in the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #) holds
a /\ b in the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #) ) )
thus  for a being Subset-Family of TopStruct(# [: the carrier of X, the carrier of Y:],t #) st a c= the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #) holds
union a in the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #) ::_thesis: for a, b being Subset of TopStruct(# [: the carrier of X, the carrier of Y:],t #) st a in the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #) & b in the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #) holds
a /\ b in the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #)
proof
let a be Subset-Family of TopStruct(# [: the carrier of X, the carrier of Y:],t #); ::_thesis: ( a c= the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #) implies union a in the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #) )
set A =  {  [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y & ex x being set st
( x in a & [:X1,Y1:] c= x ) )  }  ;
  {  [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y & ex x being set st
( x in a & [:X1,Y1:] c= x ) )  }  c= bool [: the carrier of X, the carrier of Y:]
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in  {  [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y & ex x being set st
( x in a & [:X1,Y1:] c= x ) )  }  or e in bool [: the carrier of X, the carrier of Y:] )
assume  e in  {  [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y & ex x being set st
( x in a & [:X1,Y1:] c= x ) )  }  ; ::_thesis: e in bool [: the carrier of X, the carrier of Y:]
then  ex X1 being Subset of X ex Y1 being Subset of Y st
( e = [:X1,Y1:] & X1 in the topology of X & Y1 in the topology of Y & ex x being set st
( x in a & [:X1,Y1:] c= x ) ) ;
hence  e in bool [: the carrier of X, the carrier of Y:] ; ::_thesis: verum
end;
then reconsider A =  {  [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y & ex x being set st
( x in a & [:X1,Y1:] c= x ) )  }  as Subset-Family of [: the carrier of X, the carrier of Y:] ;
assume A3: a c= the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #) ; ::_thesis: union a in the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #)
A4: union A = union a
proof
thus  union A c= union a :: according to XBOOLE_0:def_10 ::_thesis: union a c= union A
proof
let e1, e2 be set ; :: according to RELAT_1:def_3 ::_thesis: ( not [e1,e2] in union A or [e1,e2] in union a )
assume  [e1,e2] in union A ; ::_thesis: [e1,e2] in union a
then consider u being set  such that
A5: [e1,e2] in u and
A6: u in A by TARSKI:def_4;
 ex X1 being Subset of X ex Y1 being Subset of Y st
( u = [:X1,Y1:] & X1 in the topology of X & Y1 in the topology of Y & ex x being set st
( x in a & [:X1,Y1:] c= x ) ) by A6;
hence  [e1,e2] in union a by A5, TARSKI:def_4; ::_thesis: verum
end;
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in union a or e in union A )
assume  e in union a ; ::_thesis: e in union A
then consider u being set  such that
A7: e in u and
A8: u in a by TARSKI:def_4;
 u in the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #) by A3, A8;
then consider B being Subset-Family of [: the carrier of X, the carrier of Y:] such that
A9: u = union B and
A10: B c=  {  [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y )  }  ;
consider x being set  such that
A11: e in x and
A12: x in B by A7, A9, TARSKI:def_4;
 x in  {  [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y )  }  by A10, A12;
then consider X1 being Subset of X, Y1 being Subset of Y such that
A13: x = [:X1,Y1:] and
A14: ( X1 in the topology of X & Y1 in the topology of Y ) ;
 [:X1,Y1:] c= u by A9, A12, A13, ZFMISC_1:74;
then  x in A by A8, A13, A14;
hence  e in union A by A11, TARSKI:def_4; ::_thesis: verum
end;
 A c=  {  [:X2,Y2:] where X2 is Subset of X, Y2 is Subset of Y : ( X2 in the topology of X & Y2 in the topology of Y )  }
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in A or e in  {  [:X2,Y2:] where X2 is Subset of X, Y2 is Subset of Y : ( X2 in the topology of X & Y2 in the topology of Y )  }  )
assume  e in A ; ::_thesis: e in  {  [:X2,Y2:] where X2 is Subset of X, Y2 is Subset of Y : ( X2 in the topology of X & Y2 in the topology of Y )  }
then  ex X1 being Subset of X ex Y1 being Subset of Y st
( e = [:X1,Y1:] & X1 in the topology of X & Y1 in the topology of Y & ex x being set st
( x in a & [:X1,Y1:] c= x ) ) ;
hence  e in  {  [:X2,Y2:] where X2 is Subset of X, Y2 is Subset of Y : ( X2 in the topology of X & Y2 in the topology of Y )  }  ; ::_thesis: verum
end;
hence  union a in the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #) by A4; ::_thesis: verum
end;
let a, b be Subset of TopStruct(# [: the carrier of X, the carrier of Y:],t #); ::_thesis: ( a in the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #) & b in the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #) implies a /\ b in the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #) )
set C =  {  [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y & [:X1,Y1:] c= a /\ b )  }  ;
  {  [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y & [:X1,Y1:] c= a /\ b )  }  c= bool [: the carrier of X, the carrier of Y:]
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in  {  [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y & [:X1,Y1:] c= a /\ b )  }  or e in bool [: the carrier of X, the carrier of Y:] )
assume  e in  {  [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y & [:X1,Y1:] c= a /\ b )  }  ; ::_thesis: e in bool [: the carrier of X, the carrier of Y:]
then  ex X1 being Subset of X ex Y1 being Subset of Y st
( e = [:X1,Y1:] & X1 in the topology of X & Y1 in the topology of Y & [:X1,Y1:] c= a /\ b ) ;
hence  e in bool [: the carrier of X, the carrier of Y:] ; ::_thesis: verum
end;
then reconsider C =  {  [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y & [:X1,Y1:] c= a /\ b )  }  as Subset-Family of [: the carrier of X, the carrier of Y:] ;
assume that
A15: a in the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #) and
A16: b in the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #) ; ::_thesis: a /\ b in the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #)
consider A being Subset-Family of [: the carrier of X, the carrier of Y:] such that
A17: a = union A and
A18: A c=  {  [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y )  }  by A15;
consider B being Subset-Family of [: the carrier of X, the carrier of Y:] such that
A19: b = union B and
A20: B c=  {  [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y )  }  by A16;
A21: a /\ b = union C
proof
thus  a /\ b c= union C :: according to XBOOLE_0:def_10 ::_thesis: union C c= a /\ b
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in a /\ b or e in union C )
assume A22: e in a /\ b ; ::_thesis: e in union C
then  e in a by XBOOLE_0:def_4;
then consider u1 being set  such that
A23: e in u1 and
A24: u1 in A by A17, TARSKI:def_4;
A25: u1 in  {  [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y )  }  by A18, A24;
 e in b by A22, XBOOLE_0:def_4;
then consider u2 being set  such that
A26: e in u2 and
A27: u2 in B by A19, TARSKI:def_4;
A28: u2 in  {  [:X2,Y2:] where X2 is Subset of X, Y2 is Subset of Y : ( X2 in the topology of X & Y2 in the topology of Y )  }  by A20, A27;
A29: u2 c= b by A19, A27, ZFMISC_1:74;
consider X1 being Subset of X, Y1 being Subset of Y such that
A30: u1 = [:X1,Y1:] and
A31: ( X1 in the topology of X & Y1 in the topology of Y ) by A25;
consider X2 being Subset of X, Y2 being Subset of Y such that
A32: u2 = [:X2,Y2:] and
A33: ( X2 in the topology of X & Y2 in the topology of Y ) by A28;
 u1 c= a by A17, A24, ZFMISC_1:74;
then  [:X1,Y1:] /\ [:X2,Y2:] c= a /\ b by A30, A32, A29, XBOOLE_1:27;
then A34: [:(X1 /\ X2),(Y1 /\ Y2):] c= a /\ b by ZFMISC_1:100;
 ( X1 /\ X2 in the topology of X & Y1 /\ Y2 in the topology of Y ) by A31, A33, PRE_TOPC:def_1;
then A35: [:(X1 /\ X2),(Y1 /\ Y2):] in C by A34;
 e in [:(X1 /\ X2),(Y1 /\ Y2):] by A23, A26, A30, A32, ZFMISC_1:113;
hence  e in union C by A35, TARSKI:def_4; ::_thesis: verum
end;
let e1, e2 be set ; :: according to RELAT_1:def_3 ::_thesis: ( not [e1,e2] in union C or [e1,e2] in a /\ b )
assume  [e1,e2] in union C ; ::_thesis: [e1,e2] in a /\ b
then consider u being set  such that
A36: [e1,e2] in u and
A37: u in C by TARSKI:def_4;
 ex X1 being Subset of X ex Y1 being Subset of Y st
( u = [:X1,Y1:] & X1 in the topology of X & Y1 in the topology of Y & [:X1,Y1:] c= a /\ b ) by A37;
hence  [e1,e2] in a /\ b by A36; ::_thesis: verum
end;
 C c=  {  [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y )  }
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in C or e in  {  [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y )  }  )
assume  e in C ; ::_thesis: e in  {  [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y )  }
then  ex X1 being Subset of X ex Y1 being Subset of Y st
( e = [:X1,Y1:] & X1 in the topology of X & Y1 in the topology of Y & [:X1,Y1:] c= a /\ b ) ;
hence  e in  {  [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y )  }  ; ::_thesis: verum
end;
hence  a /\ b in the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #) by A21; ::_thesis: verum
end;
then reconsider T = TopStruct(# [: the carrier of X, the carrier of Y:],t #) as strict TopSpace by PRE_TOPC:def_1;
take  T ; ::_thesis: ( the carrier of T = [: the carrier of X, the carrier of Y:] & the topology of T =  {  (union A) where A is Subset-Family of T : A c=  {  [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y )  }   }  )
thus  ( the carrier of T = [: the carrier of X, the carrier of Y:] & the topology of T =  {  (union A) where A is Subset-Family of T : A c=  {  [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y )  }   }  ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being strict TopSpace st the carrier of b1 = [: the carrier of X, the carrier of Y:] & the topology of b1 =  {  (union A) where A is Subset-Family of b1 : A c=  {  [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y )  }   }  & the carrier of b2 = [: the carrier of X, the carrier of Y:] & the topology of b2 =  {  (union A) where A is Subset-Family of b2 : A c=  {  [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y )  }   }  holds
b1 = b2 ;
end;

:: deftheorem Def2 defines [: BORSUK_1:def_2_:_
 for X, Y being TopSpace
for b3 being strict TopSpace holds
( b3 = [:X,Y:] iff ( the carrier of b3 = [: the carrier of X, the carrier of Y:] & the topology of b3 =  {  (union A) where A is Subset-Family of b3 : A c=  {  [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y )  }   }  ) );

registration
let T1 be TopSpace;
let T2 be empty TopSpace;
cluster[:T1,T2:] ->  empty strict ;
coherence
 [:T1,T2:] is empty
proof
 the carrier of [:T1,T2:] = [: the carrier of T1, the carrier of T2:] by Def2;
hence  [:T1,T2:] is empty ; ::_thesis: verum
end;
cluster[:T2,T1:] ->  empty strict ;
coherence
 [:T2,T1:] is empty
proof
 the carrier of [:T2,T1:] = [: the carrier of T2, the carrier of T1:] by Def2;
hence  [:T2,T1:] is empty ; ::_thesis: verum
end;
end;

registration
let X, Y be non empty TopSpace;
cluster[:X,Y:] ->  non empty strict ;
coherence
 not [:X,Y:] is empty
proof
 the carrier of [:X,Y:] = [: the carrier of X, the carrier of Y:] by Def2;
hence  not the carrier of [:X,Y:] is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum
end;
end;

theorem Th5: :: BORSUK_1:5
for X, Y being TopSpace
for B being Subset of [:X,Y:] holds
( B is open iff ex A being Subset-Family of [:X,Y:] st
( B = union A & ( for e being set st e in A holds
ex X1 being Subset of X ex Y1 being Subset of Y st
( e = [:X1,Y1:] & X1 is open & Y1 is open ) ) ) )
proof
let X, Y be TopSpace; ::_thesis: for B being Subset of [:X,Y:] holds
( B is open iff ex A being Subset-Family of [:X,Y:] st
( B = union A & ( for e being set st e in A holds
ex X1 being Subset of X ex Y1 being Subset of Y st
( e = [:X1,Y1:] & X1 is open & Y1 is open ) ) ) )
let B be Subset of [:X,Y:]; ::_thesis: ( B is open iff ex A being Subset-Family of [:X,Y:] st
( B = union A & ( for e being set st e in A holds
ex X1 being Subset of X ex Y1 being Subset of Y st
( e = [:X1,Y1:] & X1 is open & Y1 is open ) ) ) )
A1: the topology of [:X,Y:] =  {  (union A) where A is Subset-Family of [:X,Y:] : A c=  {  [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y )  }   }  by Def2;
thus  ( B is open implies ex A being Subset-Family of [:X,Y:] st
( B = union A & ( for e being set st e in A holds
ex X1 being Subset of X ex Y1 being Subset of Y st
( e = [:X1,Y1:] & X1 is open & Y1 is open ) ) ) ) ::_thesis: ( ex A being Subset-Family of [:X,Y:] st
( B = union A & ( for e being set st e in A holds
ex X1 being Subset of X ex Y1 being Subset of Y st
( e = [:X1,Y1:] & X1 is open & Y1 is open ) ) ) implies B is open )
proof
assume  B in the topology of [:X,Y:] ; :: according to PRE_TOPC:def_2 ::_thesis: ex A being Subset-Family of [:X,Y:] st
( B = union A & ( for e being set st e in A holds
ex X1 being Subset of X ex Y1 being Subset of Y st
( e = [:X1,Y1:] & X1 is open & Y1 is open ) ) )
then consider A being Subset-Family of [:X,Y:] such that
A2: B = union A and
A3: A c=  {  [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y )  }  by A1;
take  A ; ::_thesis: ( B = union A & ( for e being set st e in A holds
ex X1 being Subset of X ex Y1 being Subset of Y st
( e = [:X1,Y1:] & X1 is open & Y1 is open ) ) )
thus  B = union A by A2; ::_thesis: for e being set st e in A holds
ex X1 being Subset of X ex Y1 being Subset of Y st
( e = [:X1,Y1:] & X1 is open & Y1 is open )
let e be set ; ::_thesis: ( e in A implies ex X1 being Subset of X ex Y1 being Subset of Y st
( e = [:X1,Y1:] & X1 is open & Y1 is open ) )
assume  e in A ; ::_thesis: ex X1 being Subset of X ex Y1 being Subset of Y st
( e = [:X1,Y1:] & X1 is open & Y1 is open )
then  e in  {  [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y )  }  by A3;
then consider X1 being Subset of X, Y1 being Subset of Y such that
A4: ( e = [:X1,Y1:] & X1 in the topology of X & Y1 in the topology of Y ) ;
reconsider Y1 = Y1 as Subset of Y ;
reconsider X1 = X1 as Subset of X ;
take  X1 ; ::_thesis: ex Y1 being Subset of Y st
( e = [:X1,Y1:] & X1 is open & Y1 is open )
take  Y1 ; ::_thesis: ( e = [:X1,Y1:] & X1 is open & Y1 is open )
thus  ( e = [:X1,Y1:] & X1 is open & Y1 is open ) by A4, PRE_TOPC:def_2; ::_thesis: verum
end;
given A being Subset-Family of [:X,Y:] such that A5: B = union A and
A6: for e being set st e in A holds
ex X1 being Subset of X ex Y1 being Subset of Y st
( e = [:X1,Y1:] & X1 is open & Y1 is open ) ; ::_thesis: B is open
 A c=  {  [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y )  }
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in A or e in  {  [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y )  }  )
assume  e in A ; ::_thesis: e in  {  [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y )  }
then consider X1 being Subset of X, Y1 being Subset of Y such that
A7: e = [:X1,Y1:] and
A8: ( X1 is open & Y1 is open ) by A6;
 ( X1 in the topology of X & Y1 in the topology of Y ) by A8, PRE_TOPC:def_2;
hence  e in  {  [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y )  }  by A7; ::_thesis: verum
end;
hence  B in the topology of [:X,Y:] by A1, A5; :: according to PRE_TOPC:def_2 ::_thesis: verum
end;

definition
let X, Y be TopSpace;
let A be Subset of X;
let B be Subset of Y;
:: original: [:
redefine func[:A,B:] ->  Subset of [:X,Y:];
correctness
coherence
[:A,B:] is Subset of [:X,Y:];
proof
thus  [:A,B:] is Subset of [:X,Y:] by Def2; ::_thesis: verum
end;
end;

definition
let X, Y be non empty TopSpace;
let x be Point of X;
let y be Point of Y;
:: original: [
redefine func[x,y] ->  Point of [:X,Y:];
correctness
coherence
[x,y] is Point of [:X,Y:];
proof
thus  [x,y] is Point of [:X,Y:] by Def2; ::_thesis: verum
end;
end;

theorem Th6: :: BORSUK_1:6
for X, Y being TopSpace
for V being Subset of X
for W being Subset of Y st V is open & W is open holds
[:V,W:] is open
proof
let X, Y be TopSpace; ::_thesis: for V being Subset of X
for W being Subset of Y st V is open & W is open holds
[:V,W:] is open
let V be Subset of X; ::_thesis: for W being Subset of Y st V is open & W is open holds
[:V,W:] is open
let W be Subset of Y; ::_thesis: ( V is open & W is open implies [:V,W:] is open )
assume A1: ( V is open & W is open ) ; ::_thesis: [:V,W:] is open
reconsider PP = {[:V,W:]} as Subset-Family of [:X,Y:] ;
reconsider PP = PP as Subset-Family of [:X,Y:] ;
A2: now__::_thesis:_for_e_being_set_st_e_in_PP_holds_
ex_V_being_Subset_of_X_ex_W_being_Subset_of_Y_st_
(_e_=_[:V,W:]_&_V_is_open_&_W_is_open_)
let e be set ; ::_thesis: ( e in PP implies ex V being Subset of X ex W being Subset of Y st
( e = [:V,W:] & V is open & W is open ) )
assume A3: e in PP ; ::_thesis: ex V being Subset of X ex W being Subset of Y st
( e = [:V,W:] & V is open & W is open )
take V = V; ::_thesis: ex W being Subset of Y st
( e = [:V,W:] & V is open & W is open )
take W = W; ::_thesis: ( e = [:V,W:] & V is open & W is open )
thus  ( e = [:V,W:] & V is open & W is open ) by A1, A3, TARSKI:def_1; ::_thesis: verum
end;
 [:V,W:] = union {[:V,W:]} by ZFMISC_1:25;
hence  [:V,W:] is open by A2, Th5; ::_thesis: verum
end;

theorem Th7: :: BORSUK_1:7
for X, Y being TopSpace
for V being Subset of X
for W being Subset of Y holds Int [:V,W:] = [:(Int V),(Int W):]
proof
let X, Y be TopSpace; ::_thesis: for V being Subset of X
for W being Subset of Y holds Int [:V,W:] = [:(Int V),(Int W):]
let V be Subset of X; ::_thesis: for W being Subset of Y holds Int [:V,W:] = [:(Int V),(Int W):]
let W be Subset of Y; ::_thesis: Int [:V,W:] = [:(Int V),(Int W):]
thus  Int [:V,W:] c= [:(Int V),(Int W):] :: according to XBOOLE_0:def_10 ::_thesis: [:(Int V),(Int W):] c= Int [:V,W:]
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in Int [:V,W:] or e in [:(Int V),(Int W):] )
assume  e in Int [:V,W:] ; ::_thesis: e in [:(Int V),(Int W):]
then consider Q being Subset of [:X,Y:] such that
A1: Q is open and
A2: Q c= [:V,W:] and
A3: e in Q by TOPS_1:22;
consider A being Subset-Family of [:X,Y:] such that
A4: Q = union A and
A5: for e being set st e in A holds
ex X1 being Subset of X ex Y1 being Subset of Y st
( e = [:X1,Y1:] & X1 is open & Y1 is open ) by A1, Th5;
consider a being set  such that
A6: e in a and
A7: a in A by A3, A4, TARSKI:def_4;
consider X1 being Subset of X, Y1 being Subset of Y such that
A8: a = [:X1,Y1:] and
A9: X1 is open and
A10: Y1 is open by A5, A7;
 [:X1,Y1:] c= Q by A4, A7, A8, ZFMISC_1:74;
then A11: [:X1,Y1:] c= [:V,W:] by A2, XBOOLE_1:1;
then  Y1 c= W by A6, A8, ZFMISC_1:114;
then A12: Y1 c= Int W by A10, TOPS_1:24;
 X1 c= V by A6, A8, A11, ZFMISC_1:114;
then  X1 c= Int V by A9, TOPS_1:24;
then  [:X1,Y1:] c= [:(Int V),(Int W):] by A12, ZFMISC_1:96;
hence  e in [:(Int V),(Int W):] by A6, A8; ::_thesis: verum
end;
 ( Int V c= V & Int W c= W ) by TOPS_1:16;
then  [:(Int V),(Int W):] c= [:V,W:] by ZFMISC_1:96;
hence  [:(Int V),(Int W):] c= Int [:V,W:] by Th6, TOPS_1:24; ::_thesis: verum
end;

theorem Th8: :: BORSUK_1:8
for X, Y being non empty TopSpace
for x being Point of X
for y being Point of Y
for V being a_neighborhood of x
for W being a_neighborhood of y holds [:V,W:] is a_neighborhood of [x,y]
proof
let X, Y be non empty TopSpace; ::_thesis: for x being Point of X
for y being Point of Y
for V being a_neighborhood of x
for W being a_neighborhood of y holds [:V,W:] is a_neighborhood of [x,y]
let x be Point of X; ::_thesis: for y being Point of Y
for V being a_neighborhood of x
for W being a_neighborhood of y holds [:V,W:] is a_neighborhood of [x,y]
let y be Point of Y; ::_thesis: for V being a_neighborhood of x
for W being a_neighborhood of y holds [:V,W:] is a_neighborhood of [x,y]
let V be a_neighborhood of x; ::_thesis: for W being a_neighborhood of y holds [:V,W:] is a_neighborhood of [x,y]
let W be a_neighborhood of y; ::_thesis: [:V,W:] is a_neighborhood of [x,y]
 ( x in Int V & y in Int W ) by CONNSP_2:def_1;
then  [x,y] in [:(Int V),(Int W):] by ZFMISC_1:87;
hence  [x,y] in Int [:V,W:] by Th7; :: according to CONNSP_2:def_1 ::_thesis: verum
end;

theorem Th9: :: BORSUK_1:9
for X, Y being non empty TopSpace
for A being Subset of X
for B being Subset of Y
for V being a_neighborhood of A
for W being a_neighborhood of B holds [:V,W:] is a_neighborhood of [:A,B:]
proof
let X, Y be non empty TopSpace; ::_thesis: for A being Subset of X
for B being Subset of Y
for V being a_neighborhood of A
for W being a_neighborhood of B holds [:V,W:] is a_neighborhood of [:A,B:]
let A be Subset of X; ::_thesis: for B being Subset of Y
for V being a_neighborhood of A
for W being a_neighborhood of B holds [:V,W:] is a_neighborhood of [:A,B:]
let B be Subset of Y; ::_thesis: for V being a_neighborhood of A
for W being a_neighborhood of B holds [:V,W:] is a_neighborhood of [:A,B:]
let V be a_neighborhood of A; ::_thesis: for W being a_neighborhood of B holds [:V,W:] is a_neighborhood of [:A,B:]
let W be a_neighborhood of B; ::_thesis: [:V,W:] is a_neighborhood of [:A,B:]
 ( A c= Int V & B c= Int W ) by CONNSP_2:def_2;
then  [:A,B:] c= [:(Int V),(Int W):] by ZFMISC_1:96;
hence  [:A,B:] c= Int [:V,W:] by Th7; :: according to CONNSP_2:def_2 ::_thesis: verum
end;

definition
let X, Y be non empty TopSpace;
let x be Point of X;
let y be Point of Y;
let V be a_neighborhood of x;
let W be a_neighborhood of y;
:: original: [:
redefine func[:V,W:] ->  a_neighborhood of [x,y];
correctness
coherence
[:V,W:] is a_neighborhood of [x,y];
by Th8;
end;

theorem Th10: :: BORSUK_1:10
for X, Y being non empty TopSpace
for XT being Point of [:X,Y:] ex W being Point of X ex T being Point of Y st XT = [W,T]
proof
let X, Y be non empty TopSpace; ::_thesis: for XT being Point of [:X,Y:] ex W being Point of X ex T being Point of Y st XT = [W,T]
let XT be Point of [:X,Y:]; ::_thesis: ex W being Point of X ex T being Point of Y st XT = [W,T]
 the carrier of [:X,Y:] = [: the carrier of X, the carrier of Y:] by Def2;
hence  ex W being Point of X ex T being Point of Y st XT = [W,T] by DOMAIN_1:1; ::_thesis: verum
end;

definition
let X, Y be non empty TopSpace;
let A be Subset of X;
let t be Point of Y;
let V be a_neighborhood of A;
let W be a_neighborhood of t;
:: original: [:
redefine func[:V,W:] ->  a_neighborhood of [:A,{t}:];
correctness
coherence
[:V,W:] is a_neighborhood of [:A,{t}:];
proof
 W is a_neighborhood of {t} by CONNSP_2:8;
hence  [:V,W:] is a_neighborhood of [:A,{t}:] by Th9; ::_thesis: verum
end;
end;

definition
let X, Y be TopSpace;
let A be Subset of [:X,Y:];
func Base-Appr A ->  Subset-Family of [:X,Y:] equals :: BORSUK_1:def 3
 {  [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( [:X1,Y1:] c= A & X1 is open & Y1 is open )  }  ;
coherence
  {  [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( [:X1,Y1:] c= A & X1 is open & Y1 is open )  }  is Subset-Family of [:X,Y:]
proof
set B =  {  [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( [:X1,Y1:] c= A & X1 is open & Y1 is open )  }  ;
  {  [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( [:X1,Y1:] c= A & X1 is open & Y1 is open )  }  c= bool the carrier of [:X,Y:]
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in  {  [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( [:X1,Y1:] c= A & X1 is open & Y1 is open )  }  or e in bool the carrier of [:X,Y:] )
assume  e in  {  [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( [:X1,Y1:] c= A & X1 is open & Y1 is open )  }  ; ::_thesis: e in bool the carrier of [:X,Y:]
then  ex X1 being Subset of X ex Y1 being Subset of Y st
( e = [:X1,Y1:] & [:X1,Y1:] c= A & X1 is open & Y1 is open ) ;
hence  e in bool the carrier of [:X,Y:] ; ::_thesis: verum
end;
hence   {  [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( [:X1,Y1:] c= A & X1 is open & Y1 is open )  }  is Subset-Family of [:X,Y:] ; ::_thesis: verum
end;
end;

:: deftheorem  defines Base-Appr BORSUK_1:def_3_:_
 for X, Y being TopSpace
for A being Subset of [:X,Y:] holds Base-Appr A =  {  [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( [:X1,Y1:] c= A & X1 is open & Y1 is open )  }  ;

registration
let X, Y be TopSpace;
let A be Subset of [:X,Y:];
cluster Base-Appr A ->  open ;
coherence
 Base-Appr A is open
proof
let B be Subset of [:X,Y:]; :: according to TOPS_2:def_1 ::_thesis: ( not B in Base-Appr A or B is open )
assume  B in Base-Appr A ; ::_thesis: B is open
then  ex X1 being Subset of X ex Y1 being Subset of Y st
( B = [:X1,Y1:] & [:X1,Y1:] c= A & X1 is open & Y1 is open ) ;
hence  B is open by Th6; ::_thesis: verum
end;
end;

theorem Th11: :: BORSUK_1:11
for X, Y being TopSpace
for A, B being Subset of [:X,Y:] st A c= B holds
Base-Appr A c= Base-Appr B
proof
let X, Y be TopSpace; ::_thesis: for A, B being Subset of [:X,Y:] st A c= B holds
Base-Appr A c= Base-Appr B
let A, B be Subset of [:X,Y:]; ::_thesis: ( A c= B implies Base-Appr A c= Base-Appr B )
assume A1: A c= B ; ::_thesis: Base-Appr A c= Base-Appr B
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in Base-Appr A or e in Base-Appr B )
assume  e in Base-Appr A ; ::_thesis: e in Base-Appr B
then consider X1 being Subset of X, Y1 being Subset of Y such that
A2: e = [:X1,Y1:] and
A3: [:X1,Y1:] c= A and
A4: ( X1 is open & Y1 is open ) ;
 [:X1,Y1:] c= B by A1, A3, XBOOLE_1:1;
hence  e in Base-Appr B by A2, A4; ::_thesis: verum
end;

theorem Th12: :: BORSUK_1:12
for X, Y being TopSpace
for A being Subset of [:X,Y:] holds union (Base-Appr A) c= A
proof
let X, Y be TopSpace; ::_thesis: for A being Subset of [:X,Y:] holds union (Base-Appr A) c= A
let A be Subset of [:X,Y:]; ::_thesis: union (Base-Appr A) c= A
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in union (Base-Appr A) or e in A )
assume  e in union (Base-Appr A) ; ::_thesis: e in A
then consider B being set  such that
A1: e in B and
A2: B in Base-Appr A by TARSKI:def_4;
 ex X1 being Subset of X ex Y1 being Subset of Y st
( B = [:X1,Y1:] & [:X1,Y1:] c= A & X1 is open & Y1 is open ) by A2;
hence  e in A by A1; ::_thesis: verum
end;

theorem Th13: :: BORSUK_1:13
for X, Y being TopSpace
for A being Subset of [:X,Y:] st A is open holds
A = union (Base-Appr A)
proof
let X, Y be TopSpace; ::_thesis: for A being Subset of [:X,Y:] st A is open holds
A = union (Base-Appr A)
let A be Subset of [:X,Y:]; ::_thesis: ( A is open implies A = union (Base-Appr A) )
assume  A is open ; ::_thesis: A = union (Base-Appr A)
then consider B being Subset-Family of [:X,Y:] such that
A1: A = union B and
A2: for e being set st e in B holds
ex X1 being Subset of X ex Y1 being Subset of Y st
( e = [:X1,Y1:] & X1 is open & Y1 is open ) by Th5;
thus  A c= union (Base-Appr A) :: according to XBOOLE_0:def_10 ::_thesis: union (Base-Appr A) c= A
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in A or e in union (Base-Appr A) )
assume  e in A ; ::_thesis: e in union (Base-Appr A)
then consider u being set  such that
A3: e in u and
A4: u in B by A1, TARSKI:def_4;
 ( ex X1 being Subset of X ex Y1 being Subset of Y st
( u = [:X1,Y1:] & X1 is open & Y1 is open ) & u c= A ) by A1, A2, A4, ZFMISC_1:74;
then  u in Base-Appr A ;
hence  e in union (Base-Appr A) by A3, TARSKI:def_4; ::_thesis: verum
end;
thus  union (Base-Appr A) c= A by Th12; ::_thesis: verum
end;

theorem Th14: :: BORSUK_1:14
for X, Y being TopSpace
for A being Subset of [:X,Y:] holds Int A = union (Base-Appr A)
proof
let X, Y be TopSpace; ::_thesis: for A being Subset of [:X,Y:] holds Int A = union (Base-Appr A)
let A be Subset of [:X,Y:]; ::_thesis: Int A = union (Base-Appr A)
 ( Int A = union (Base-Appr (Int A)) & Base-Appr (Int A) c= Base-Appr A ) by Th11, Th13, TOPS_1:16;
hence  Int A c= union (Base-Appr A) by ZFMISC_1:77; :: according to XBOOLE_0:def_10 ::_thesis: union (Base-Appr A) c= Int A
 union (Base-Appr A) is open by TOPS_2:19;
hence  union (Base-Appr A) c= Int A by Th12, TOPS_1:24; ::_thesis: verum
end;

definition
let X, Y be non empty TopSpace;
func Pr1 (X,Y) ->  Function of (bool the carrier of [:X,Y:]),(bool the carrier of X) equals :: BORSUK_1:def 4
 .: (pr1 ( the carrier of X, the carrier of Y));
coherence
 .: (pr1 ( the carrier of X, the carrier of Y)) is Function of (bool the carrier of [:X,Y:]),(bool the carrier of X)
proof
 the carrier of [:X,Y:] = [: the carrier of X, the carrier of Y:] by Def2;
hence  .: (pr1 ( the carrier of X, the carrier of Y)) is Function of (bool the carrier of [:X,Y:]),(bool the carrier of X) ; ::_thesis: verum
end;
correctness
;
func Pr2 (X,Y) ->  Function of (bool the carrier of [:X,Y:]),(bool the carrier of Y) equals :: BORSUK_1:def 5
 .: (pr2 ( the carrier of X, the carrier of Y));
coherence
 .: (pr2 ( the carrier of X, the carrier of Y)) is Function of (bool the carrier of [:X,Y:]),(bool the carrier of Y)
proof
 the carrier of [:X,Y:] = [: the carrier of X, the carrier of Y:] by Def2;
hence  .: (pr2 ( the carrier of X, the carrier of Y)) is Function of (bool the carrier of [:X,Y:]),(bool the carrier of Y) ; ::_thesis: verum
end;
correctness
;
end;

:: deftheorem  defines Pr1 BORSUK_1:def_4_:_
 for X, Y being non empty TopSpace holds Pr1 (X,Y) = .: (pr1 ( the carrier of X, the carrier of Y));

:: deftheorem  defines Pr2 BORSUK_1:def_5_:_
 for X, Y being non empty TopSpace holds Pr2 (X,Y) = .: (pr2 ( the carrier of X, the carrier of Y));

theorem Th15: :: BORSUK_1:15
for X, Y being non empty TopSpace
for A being Subset of [:X,Y:]
for H being Subset-Family of [:X,Y:] st ( for e being set st e in H holds
( e c= A & ex X1 being Subset of X ex Y1 being Subset of Y st e = [:X1,Y1:] ) ) holds
[:(union ((Pr1 (X,Y)) .: H)),(meet ((Pr2 (X,Y)) .: H)):] c= A
proof
let X, Y be non empty TopSpace; ::_thesis: for A being Subset of [:X,Y:]
for H being Subset-Family of [:X,Y:] st ( for e being set st e in H holds
( e c= A & ex X1 being Subset of X ex Y1 being Subset of Y st e = [:X1,Y1:] ) ) holds
[:(union ((Pr1 (X,Y)) .: H)),(meet ((Pr2 (X,Y)) .: H)):] c= A
let A be Subset of [:X,Y:]; ::_thesis: for H being Subset-Family of [:X,Y:] st ( for e being set st e in H holds
( e c= A & ex X1 being Subset of X ex Y1 being Subset of Y st e = [:X1,Y1:] ) ) holds
[:(union ((Pr1 (X,Y)) .: H)),(meet ((Pr2 (X,Y)) .: H)):] c= A
let H be Subset-Family of [:X,Y:]; ::_thesis: ( ( for e being set st e in H holds
( e c= A & ex X1 being Subset of X ex Y1 being Subset of Y st e = [:X1,Y1:] ) ) implies [:(union ((Pr1 (X,Y)) .: H)),(meet ((Pr2 (X,Y)) .: H)):] c= A )
assume A1: for e being set st e in H holds
( e c= A & ex X1 being Subset of X ex Y1 being Subset of Y st e = [:X1,Y1:] ) ; ::_thesis: [:(union ((Pr1 (X,Y)) .: H)),(meet ((Pr2 (X,Y)) .: H)):] c= A
 the carrier of [:X,Y:] = [: the carrier of X, the carrier of Y:] by Def2;
hence  [:(union ((Pr1 (X,Y)) .: H)),(meet ((Pr2 (X,Y)) .: H)):] c= A by A1, EQREL_1:51; ::_thesis: verum
end;

theorem Th16: :: BORSUK_1:16
for X, Y being non empty TopSpace
for H being Subset-Family of [:X,Y:]
for C being set st C in (Pr1 (X,Y)) .: H holds
ex D being Subset of [:X,Y:] st
( D in H & C = (pr1 ( the carrier of X, the carrier of Y)) .: D )
proof
let X, Y be non empty TopSpace; ::_thesis: for H being Subset-Family of [:X,Y:]
for C being set st C in (Pr1 (X,Y)) .: H holds
ex D being Subset of [:X,Y:] st
( D in H & C = (pr1 ( the carrier of X, the carrier of Y)) .: D )
let H be Subset-Family of [:X,Y:]; ::_thesis: for C being set st C in (Pr1 (X,Y)) .: H holds
ex D being Subset of [:X,Y:] st
( D in H & C = (pr1 ( the carrier of X, the carrier of Y)) .: D )
let C be set ; ::_thesis: ( C in (Pr1 (X,Y)) .: H implies ex D being Subset of [:X,Y:] st
( D in H & C = (pr1 ( the carrier of X, the carrier of Y)) .: D ) )
assume  C in (Pr1 (X,Y)) .: H ; ::_thesis: ex D being Subset of [:X,Y:] st
( D in H & C = (pr1 ( the carrier of X, the carrier of Y)) .: D )
then consider u being set  such that
A1: u in dom (Pr1 (X,Y)) and
A2: u in H and
A3: C = (Pr1 (X,Y)) . u by FUNCT_1:def_6;
reconsider u = u as Subset of [:X,Y:] by A1;
take  u ; ::_thesis: ( u in H & C = (pr1 ( the carrier of X, the carrier of Y)) .: u )
thus  u in H by A2; ::_thesis: C = (pr1 ( the carrier of X, the carrier of Y)) .: u
 the carrier of [:X,Y:] = [: the carrier of X, the carrier of Y:] by Def2;
hence  C = (pr1 ( the carrier of X, the carrier of Y)) .: u by A3, EQREL_1:47; ::_thesis: verum
end;

theorem Th17: :: BORSUK_1:17
for X, Y being non empty TopSpace
for H being Subset-Family of [:X,Y:]
for C being set st C in (Pr2 (X,Y)) .: H holds
ex D being Subset of [:X,Y:] st
( D in H & C = (pr2 ( the carrier of X, the carrier of Y)) .: D )
proof
let X, Y be non empty TopSpace; ::_thesis: for H being Subset-Family of [:X,Y:]
for C being set st C in (Pr2 (X,Y)) .: H holds
ex D being Subset of [:X,Y:] st
( D in H & C = (pr2 ( the carrier of X, the carrier of Y)) .: D )
let H be Subset-Family of [:X,Y:]; ::_thesis: for C being set st C in (Pr2 (X,Y)) .: H holds
ex D being Subset of [:X,Y:] st
( D in H & C = (pr2 ( the carrier of X, the carrier of Y)) .: D )
let C be set ; ::_thesis: ( C in (Pr2 (X,Y)) .: H implies ex D being Subset of [:X,Y:] st
( D in H & C = (pr2 ( the carrier of X, the carrier of Y)) .: D ) )
assume  C in (Pr2 (X,Y)) .: H ; ::_thesis: ex D being Subset of [:X,Y:] st
( D in H & C = (pr2 ( the carrier of X, the carrier of Y)) .: D )
then consider u being set  such that
A1: u in dom (Pr2 (X,Y)) and
A2: u in H and
A3: C = (Pr2 (X,Y)) . u by FUNCT_1:def_6;
reconsider u = u as Subset of [:X,Y:] by A1;
take  u ; ::_thesis: ( u in H & C = (pr2 ( the carrier of X, the carrier of Y)) .: u )
thus  u in H by A2; ::_thesis: C = (pr2 ( the carrier of X, the carrier of Y)) .: u
 the carrier of [:X,Y:] = [: the carrier of X, the carrier of Y:] by Def2;
hence  C = (pr2 ( the carrier of X, the carrier of Y)) .: u by A3, EQREL_1:48; ::_thesis: verum
end;

theorem Th18: :: BORSUK_1:18
for X, Y being non empty TopSpace
for D being Subset of [:X,Y:] st D is open holds
for X1 being Subset of X
for Y1 being Subset of Y holds
( ( X1 = (pr1 ( the carrier of X, the carrier of Y)) .: D implies X1 is open ) & ( Y1 = (pr2 ( the carrier of X, the carrier of Y)) .: D implies Y1 is open ) )
proof
let X, Y be non empty TopSpace; ::_thesis: for D being Subset of [:X,Y:] st D is open holds
for X1 being Subset of X
for Y1 being Subset of Y holds
( ( X1 = (pr1 ( the carrier of X, the carrier of Y)) .: D implies X1 is open ) & ( Y1 = (pr2 ( the carrier of X, the carrier of Y)) .: D implies Y1 is open ) )
let D be Subset of [:X,Y:]; ::_thesis: ( D is open implies for X1 being Subset of X
for Y1 being Subset of Y holds
( ( X1 = (pr1 ( the carrier of X, the carrier of Y)) .: D implies X1 is open ) & ( Y1 = (pr2 ( the carrier of X, the carrier of Y)) .: D implies Y1 is open ) ) )
set p = pr2 ( the carrier of X, the carrier of Y);
set P = .: (pr2 ( the carrier of X, the carrier of Y));
assume  D is open ; ::_thesis: for X1 being Subset of X
for Y1 being Subset of Y holds
( ( X1 = (pr1 ( the carrier of X, the carrier of Y)) .: D implies X1 is open ) & ( Y1 = (pr2 ( the carrier of X, the carrier of Y)) .: D implies Y1 is open ) )
then consider H being Subset-Family of [:X,Y:] such that
A1: D = union H and
A2: for e being set st e in H holds
ex X1 being Subset of X ex Y1 being Subset of Y st
( e = [:X1,Y1:] & X1 is open & Y1 is open ) by Th5;
reconsider K = H as Subset-Family of [: the carrier of X, the carrier of Y:] by Def2;
let X1 be Subset of X; ::_thesis: for Y1 being Subset of Y holds
( ( X1 = (pr1 ( the carrier of X, the carrier of Y)) .: D implies X1 is open ) & ( Y1 = (pr2 ( the carrier of X, the carrier of Y)) .: D implies Y1 is open ) )
let Y1 be Subset of Y; ::_thesis: ( ( X1 = (pr1 ( the carrier of X, the carrier of Y)) .: D implies X1 is open ) & ( Y1 = (pr2 ( the carrier of X, the carrier of Y)) .: D implies Y1 is open ) )
thus  ( X1 = (pr1 ( the carrier of X, the carrier of Y)) .: D implies X1 is open ) ::_thesis: ( Y1 = (pr2 ( the carrier of X, the carrier of Y)) .: D implies Y1 is open )
proof
set p = pr1 ( the carrier of X, the carrier of Y);
set P = .: (pr1 ( the carrier of X, the carrier of Y));
reconsider PK = (.: (pr1 ( the carrier of X, the carrier of Y))) .: K as Subset-Family of X ;
reconsider PK = PK as Subset-Family of X ;
A3: PK is open
proof
let X1 be Subset of X; :: according to TOPS_2:def_1 ::_thesis: ( not X1 in PK or X1 is open )
reconsider x1 = X1 as Subset of X ;
assume  X1 in PK ; ::_thesis: X1 is open
then consider c being Subset of [: the carrier of X, the carrier of Y:] such that
A4: c in K and
A5: x1 = (.: (pr1 ( the carrier of X, the carrier of Y))) . c by FUNCT_2:65;
 dom (.: (pr1 ( the carrier of X, the carrier of Y))) = bool [: the carrier of X, the carrier of Y:] by FUNCT_2:def_1;
then A6: X1 = (pr1 ( the carrier of X, the carrier of Y)) .: c by A5, FUNCT_3:7;
A7: ( c = {} or c <> {} ) ;
 ex X2 being Subset of X ex Y2 being Subset of Y st
( c = [:X2,Y2:] & X2 is open & Y2 is open ) by A2, A4;
hence  X1 is open by A6, A7, EQREL_1:49; ::_thesis: verum
end;
assume  X1 = (pr1 ( the carrier of X, the carrier of Y)) .: D ; ::_thesis: X1 is open
then  X1 = union ((.: (pr1 ( the carrier of X, the carrier of Y))) .: K) by A1, EQREL_1:53;
hence  X1 is open by A3, TOPS_2:19; ::_thesis: verum
end;
reconsider PK = (.: (pr2 ( the carrier of X, the carrier of Y))) .: K as Subset-Family of Y ;
reconsider PK = PK as Subset-Family of Y ;
A8: PK is open
proof
let Y1 be Subset of Y; :: according to TOPS_2:def_1 ::_thesis: ( not Y1 in PK or Y1 is open )
reconsider y1 = Y1 as Subset of Y ;
assume  Y1 in PK ; ::_thesis: Y1 is open
then consider c being Subset of [: the carrier of X, the carrier of Y:] such that
A9: c in K and
A10: y1 = (.: (pr2 ( the carrier of X, the carrier of Y))) . c by FUNCT_2:65;
 dom (.: (pr2 ( the carrier of X, the carrier of Y))) = bool [: the carrier of X, the carrier of Y:] by FUNCT_2:def_1;
then A11: Y1 = (pr2 ( the carrier of X, the carrier of Y)) .: c by A10, FUNCT_3:7;
A12: ( c = {} or c <> {} ) ;
 ex X2 being Subset of X ex Y2 being Subset of Y st
( c = [:X2,Y2:] & X2 is open & Y2 is open ) by A2, A9;
hence  Y1 is open by A11, A12, EQREL_1:49; ::_thesis: verum
end;
assume  Y1 = (pr2 ( the carrier of X, the carrier of Y)) .: D ; ::_thesis: Y1 is open
then  Y1 = union ((.: (pr2 ( the carrier of X, the carrier of Y))) .: K) by A1, EQREL_1:53;
hence  Y1 is open by A8, TOPS_2:19; ::_thesis: verum
end;

theorem Th19: :: BORSUK_1:19
for X, Y being non empty TopSpace
for H being Subset-Family of [:X,Y:] st H is open holds
( (Pr1 (X,Y)) .: H is open & (Pr2 (X,Y)) .: H is open )
proof
let X, Y be non empty TopSpace; ::_thesis: for H being Subset-Family of [:X,Y:] st H is open holds
( (Pr1 (X,Y)) .: H is open & (Pr2 (X,Y)) .: H is open )
let H be Subset-Family of [:X,Y:]; ::_thesis: ( H is open implies ( (Pr1 (X,Y)) .: H is open & (Pr2 (X,Y)) .: H is open ) )
reconsider P1 = (Pr1 (X,Y)) .: H as Subset-Family of X ;
reconsider P2 = (Pr2 (X,Y)) .: H as Subset-Family of Y ;
assume A1: H is open ; ::_thesis: ( (Pr1 (X,Y)) .: H is open & (Pr2 (X,Y)) .: H is open )
A2: P2 is open
proof
let Y1 be Subset of Y; :: according to TOPS_2:def_1 ::_thesis: ( not Y1 in P2 or Y1 is open )
assume  Y1 in P2 ; ::_thesis: Y1 is open
then consider D being Subset of [:X,Y:] such that
A3: D in H and
A4: Y1 = (pr2 ( the carrier of X, the carrier of Y)) .: D by Th17;
 D is open by A1, A3, TOPS_2:def_1;
hence  Y1 is open by A4, Th18; ::_thesis: verum
end;
 P1 is open
proof
let X1 be Subset of X; :: according to TOPS_2:def_1 ::_thesis: ( not X1 in P1 or X1 is open )
assume  X1 in P1 ; ::_thesis: X1 is open
then consider D being Subset of [:X,Y:] such that
A5: D in H and
A6: X1 = (pr1 ( the carrier of X, the carrier of Y)) .: D by Th16;
 D is open by A1, A5, TOPS_2:def_1;
hence  X1 is open by A6, Th18; ::_thesis: verum
end;
hence  ( (Pr1 (X,Y)) .: H is open & (Pr2 (X,Y)) .: H is open ) by A2; ::_thesis: verum
end;

theorem Th20: :: BORSUK_1:20
for X, Y being non empty TopSpace
for H being Subset-Family of [:X,Y:] st ( (Pr1 (X,Y)) .: H = {} or (Pr2 (X,Y)) .: H = {} ) holds
H = {}
proof
let X, Y be non empty TopSpace; ::_thesis: for H being Subset-Family of [:X,Y:] st ( (Pr1 (X,Y)) .: H = {} or (Pr2 (X,Y)) .: H = {} ) holds
H = {}
let H be Subset-Family of [:X,Y:]; ::_thesis: ( ( (Pr1 (X,Y)) .: H = {} or (Pr2 (X,Y)) .: H = {} ) implies H = {} )
 ( dom (Pr1 (X,Y)) = bool the carrier of [:X,Y:] & dom (Pr2 (X,Y)) = bool the carrier of [:X,Y:] ) by FUNCT_2:def_1;
hence  ( ( (Pr1 (X,Y)) .: H = {} or (Pr2 (X,Y)) .: H = {} ) implies H = {} ) ; ::_thesis: verum
end;

theorem Th21: :: BORSUK_1:21
for X, Y being non empty TopSpace
for H being Subset-Family of [:X,Y:]
for X1 being Subset of X
for Y1 being Subset of Y st H is Cover of [:X1,Y1:] holds
( ( Y1 <> {} implies (Pr1 (X,Y)) .: H is Cover of X1 ) & ( X1 <> {} implies (Pr2 (X,Y)) .: H is Cover of Y1 ) )
proof
let X, Y be non empty TopSpace; ::_thesis: for H being Subset-Family of [:X,Y:]
for X1 being Subset of X
for Y1 being Subset of Y st H is Cover of [:X1,Y1:] holds
( ( Y1 <> {} implies (Pr1 (X,Y)) .: H is Cover of X1 ) & ( X1 <> {} implies (Pr2 (X,Y)) .: H is Cover of Y1 ) )
let H be Subset-Family of [:X,Y:]; ::_thesis: for X1 being Subset of X
for Y1 being Subset of Y st H is Cover of [:X1,Y1:] holds
( ( Y1 <> {} implies (Pr1 (X,Y)) .: H is Cover of X1 ) & ( X1 <> {} implies (Pr2 (X,Y)) .: H is Cover of Y1 ) )
let X1 be Subset of X; ::_thesis: for Y1 being Subset of Y st H is Cover of [:X1,Y1:] holds
( ( Y1 <> {} implies (Pr1 (X,Y)) .: H is Cover of X1 ) & ( X1 <> {} implies (Pr2 (X,Y)) .: H is Cover of Y1 ) )
let Y1 be Subset of Y; ::_thesis: ( H is Cover of [:X1,Y1:] implies ( ( Y1 <> {} implies (Pr1 (X,Y)) .: H is Cover of X1 ) & ( X1 <> {} implies (Pr2 (X,Y)) .: H is Cover of Y1 ) ) )
A1: dom (.: (pr2 ( the carrier of X, the carrier of Y))) = bool (dom (pr2 ( the carrier of X, the carrier of Y))) by FUNCT_3:def_1
.= bool [: the carrier of X, the carrier of Y:] by FUNCT_3:def_5 ;
A2: the carrier of [:X,Y:] = [: the carrier of X, the carrier of Y:] by Def2;
assume A3: [:X1,Y1:] c= union H ; :: according to SETFAM_1:def_11 ::_thesis: ( ( Y1 <> {} implies (Pr1 (X,Y)) .: H is Cover of X1 ) & ( X1 <> {} implies (Pr2 (X,Y)) .: H is Cover of Y1 ) )
thus  ( Y1 <> {} implies (Pr1 (X,Y)) .: H is Cover of X1 ) ::_thesis: ( X1 <> {} implies (Pr2 (X,Y)) .: H is Cover of Y1 )
proof
assume  Y1 <> {} ; ::_thesis: (Pr1 (X,Y)) .: H is Cover of X1
then consider y being Point of Y such that
A4: y in Y1 by SUBSET_1:4;
let e be set ; :: according to TARSKI:def_3,SETFAM_1:def_11 ::_thesis: ( not e in X1 or e in union ((Pr1 (X,Y)) .: H) )
assume A5: e in X1 ; ::_thesis: e in union ((Pr1 (X,Y)) .: H)
then reconsider x = e as Point of X ;
 [x,y] in [:X1,Y1:] by A4, A5, ZFMISC_1:87;
then consider A being set  such that
A6: [x,y] in A and
A7: A in H by A3, TARSKI:def_4;
 [x,y] in [: the carrier of X, the carrier of Y:] by ZFMISC_1:87;
then A8: [x,y] in dom (pr1 ( the carrier of X, the carrier of Y)) by FUNCT_3:def_4;
A9: dom (.: (pr1 ( the carrier of X, the carrier of Y))) = bool (dom (pr1 ( the carrier of X, the carrier of Y))) by FUNCT_3:def_1
.= bool [: the carrier of X, the carrier of Y:] by FUNCT_3:def_4 ;
 e = (pr1 ( the carrier of X, the carrier of Y)) . (x,y) by FUNCT_3:def_4;
then A10: e in (pr1 ( the carrier of X, the carrier of Y)) .: A by A6, A8, FUNCT_1:def_6;
 (.: (pr1 ( the carrier of X, the carrier of Y))) . A = (pr1 ( the carrier of X, the carrier of Y)) .: A by A2, A7, EQREL_1:47;
then  (pr1 ( the carrier of X, the carrier of Y)) .: A in (Pr1 (X,Y)) .: H by A2, A7, A9, FUNCT_1:def_6;
hence  e in union ((Pr1 (X,Y)) .: H) by A10, TARSKI:def_4; ::_thesis: verum
end;
assume  X1 <> {} ; ::_thesis: (Pr2 (X,Y)) .: H is Cover of Y1
then consider x being Point of X such that
A11: x in X1 by SUBSET_1:4;
let e be set ; :: according to TARSKI:def_3,SETFAM_1:def_11 ::_thesis: ( not e in Y1 or e in union ((Pr2 (X,Y)) .: H) )
assume A12: e in Y1 ; ::_thesis: e in union ((Pr2 (X,Y)) .: H)
then reconsider y = e as Point of Y ;
 [x,y] in [:X1,Y1:] by A11, A12, ZFMISC_1:87;
then consider A being set  such that
A13: [x,y] in A and
A14: A in H by A3, TARSKI:def_4;
 [x,y] in [: the carrier of X, the carrier of Y:] by ZFMISC_1:87;
then A15: [x,y] in dom (pr2 ( the carrier of X, the carrier of Y)) by FUNCT_3:def_5;
 e = (pr2 ( the carrier of X, the carrier of Y)) . (x,y) by FUNCT_3:def_5;
then A16: e in (pr2 ( the carrier of X, the carrier of Y)) .: A by A13, A15, FUNCT_1:def_6;
 (.: (pr2 ( the carrier of X, the carrier of Y))) . A = (pr2 ( the carrier of X, the carrier of Y)) .: A by A2, A14, EQREL_1:48;
then  (pr2 ( the carrier of X, the carrier of Y)) .: A in (Pr2 (X,Y)) .: H by A2, A14, A1, FUNCT_1:def_6;
hence  e in union ((Pr2 (X,Y)) .: H) by A16, TARSKI:def_4; ::_thesis: verum
end;

theorem Th22: :: BORSUK_1:22
for X, Y being TopSpace
for H being Subset-Family of X
for Y being Subset of X st H is Cover of Y holds
ex F being Subset-Family of X st
( F c= H & F is Cover of Y & ( for C being set st C in F holds
C meets Y ) )
proof
let X, Y be TopSpace; ::_thesis: for H being Subset-Family of X
for Y being Subset of X st H is Cover of Y holds
ex F being Subset-Family of X st
( F c= H & F is Cover of Y & ( for C being set st C in F holds
C meets Y ) )
let H be Subset-Family of X; ::_thesis: for Y being Subset of X st H is Cover of Y holds
ex F being Subset-Family of X st
( F c= H & F is Cover of Y & ( for C being set st C in F holds
C meets Y ) )
let Y be Subset of X; ::_thesis: ( H is Cover of Y implies ex F being Subset-Family of X st
( F c= H & F is Cover of Y & ( for C being set st C in F holds
C meets Y ) ) )
assume A1: H is Cover of Y ; ::_thesis: ex F being Subset-Family of X st
( F c= H & F is Cover of Y & ( for C being set st C in F holds
C meets Y ) )
defpred S1[ set ] means ( $1 in H & $1 /\ Y <> {} );
  {  Z where Z is Subset of X : S1[Z]  }  is Subset-Family of X from DOMAIN_1:sch_7();
then reconsider F =  {  Z where Z is Subset of X : ( Z in H & Z /\ Y <> {} )  }  as Subset-Family of X ;
reconsider F = F as Subset-Family of X ;
take  F ; ::_thesis: ( F c= H & F is Cover of Y & ( for C being set st C in F holds
C meets Y ) )
thus  F c= H ::_thesis: ( F is Cover of Y & ( for C being set st C in F holds
C meets Y ) )
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in F or e in H )
assume  e in F ; ::_thesis: e in H
then  ex Z being Subset of X st
( e = Z & Z in H & Z /\ Y <> {} ) ;
hence  e in H ; ::_thesis: verum
end;
A2: Y c= union H by A1, SETFAM_1:def_11;
thus  F is Cover of Y ::_thesis: for C being set st C in F holds
C meets Y
proof
let e be set ; :: according to TARSKI:def_3,SETFAM_1:def_11 ::_thesis: ( not e in Y or e in union F )
assume A3: e in Y ; ::_thesis: e in union F
then consider u being set  such that
A4: e in u and
A5: u in H by A2, TARSKI:def_4;
reconsider u = u as Subset of X by A5;
 u /\ Y <> {} by A3, A4, XBOOLE_0:def_4;
then  u in F by A5;
hence  e in union F by A4, TARSKI:def_4; ::_thesis: verum
end;
let C be set ; ::_thesis: ( C in F implies C meets Y )
assume  C in F ; ::_thesis: C meets Y
then  ex Z being Subset of X st
( C = Z & Z in H & Z /\ Y <> {} ) ;
hence  C /\ Y <> {} ; :: according to XBOOLE_0:def_7 ::_thesis: verum
end;

theorem Th23: :: BORSUK_1:23
for X, Y being non empty TopSpace
for F being Subset-Family of X
for H being Subset-Family of [:X,Y:] st F is finite & F c= (Pr1 (X,Y)) .: H holds
ex G being Subset-Family of [:X,Y:] st
( G c= H & G is finite & F = (Pr1 (X,Y)) .: G )
proof
let X, Y be non empty TopSpace; ::_thesis: for F being Subset-Family of X
for H being Subset-Family of [:X,Y:] st F is finite & F c= (Pr1 (X,Y)) .: H holds
ex G being Subset-Family of [:X,Y:] st
( G c= H & G is finite & F = (Pr1 (X,Y)) .: G )
let F be Subset-Family of X; ::_thesis: for H being Subset-Family of [:X,Y:] st F is finite & F c= (Pr1 (X,Y)) .: H holds
ex G being Subset-Family of [:X,Y:] st
( G c= H & G is finite & F = (Pr1 (X,Y)) .: G )
let H be Subset-Family of [:X,Y:]; ::_thesis: ( F is finite & F c= (Pr1 (X,Y)) .: H implies ex G being Subset-Family of [:X,Y:] st
( G c= H & G is finite & F = (Pr1 (X,Y)) .: G ) )
assume that
A1: F is finite and
A2: F c= (Pr1 (X,Y)) .: H ; ::_thesis: ex G being Subset-Family of [:X,Y:] st
( G c= H & G is finite & F = (Pr1 (X,Y)) .: G )
defpred S1[ set , set ] means ( $2 in dom (Pr1 (X,Y)) & $2 in H & $1 = (Pr1 (X,Y)) . $2 );
A3: for e being set st e in F holds
ex u being set st S1[e,u] by A2, FUNCT_1:def_6;
consider f being Function such that
A4: dom f = F and
A5: for e being set st e in F holds
S1[e,f . e] from CLASSES1:sch_1(A3);
A6: f .: F c= H
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in f .: F or e in H )
assume  e in f .: F ; ::_thesis: e in H
then  ex u being set st
( u in dom f & u in F & e = f . u ) by FUNCT_1:def_6;
hence  e in H by A5; ::_thesis: verum
end;
then reconsider G = f .: F as Subset-Family of [:X,Y:] by XBOOLE_1:1;
take  G ; ::_thesis: ( G c= H & G is finite & F = (Pr1 (X,Y)) .: G )
thus  G c= H by A6; ::_thesis: ( G is finite & F = (Pr1 (X,Y)) .: G )
thus  G is finite by A1; ::_thesis: F = (Pr1 (X,Y)) .: G
now__::_thesis:_for_e_being_set_holds_
(_e_in_F_iff_ex_u_being_set_st_
(_u_in_dom_(Pr1_(X,Y))_&_u_in_G_&_e_=_(Pr1_(X,Y))_._u_)_)
let e be set ; ::_thesis: ( e in F iff ex u being set st
( u in dom (Pr1 (X,Y)) & u in G & e = (Pr1 (X,Y)) . u ) )
thus  ( e in F iff ex u being set st
( u in dom (Pr1 (X,Y)) & u in G & e = (Pr1 (X,Y)) . u ) ) ::_thesis: verum
proof
thus  ( e in F implies ex u being set st
( u in dom (Pr1 (X,Y)) & u in G & e = (Pr1 (X,Y)) . u ) ) ::_thesis: ( ex u being set st
( u in dom (Pr1 (X,Y)) & u in G & e = (Pr1 (X,Y)) . u ) implies e in F )
proof
assume A7: e in F ; ::_thesis: ex u being set st
( u in dom (Pr1 (X,Y)) & u in G & e = (Pr1 (X,Y)) . u )
take  f . e ; ::_thesis: ( f . e in dom (Pr1 (X,Y)) & f . e in G & e = (Pr1 (X,Y)) . (f . e) )
thus  f . e in dom (Pr1 (X,Y)) by A5, A7; ::_thesis: ( f . e in G & e = (Pr1 (X,Y)) . (f . e) )
thus  f . e in G by A4, A7, FUNCT_1:def_6; ::_thesis: e = (Pr1 (X,Y)) . (f . e)
thus  e = (Pr1 (X,Y)) . (f . e) by A5, A7; ::_thesis: verum
end;
given u being set  such that  u in dom (Pr1 (X,Y)) and
A8: u in G and
A9: e = (Pr1 (X,Y)) . u ; ::_thesis: e in F
 ex v being set st
( v in dom f & v in F & u = f . v ) by A8, FUNCT_1:def_6;
hence  e in F by A5, A9; ::_thesis: verum
end;
end;
hence  F = (Pr1 (X,Y)) .: G by FUNCT_1:def_6; ::_thesis: verum
end;

theorem :: BORSUK_1:24
for X, Y being non empty TopSpace
for X1 being Subset of X
for Y1 being Subset of Y st [:X1,Y1:] <> {} holds
( (Pr1 (X,Y)) . [:X1,Y1:] = X1 & (Pr2 (X,Y)) . [:X1,Y1:] = Y1 ) by EQREL_1:50;

theorem Th25: :: BORSUK_1:25
for Y, X being non empty TopSpace
for t being Point of Y
for A being Subset of X st A is compact holds
for G being a_neighborhood of [:A,{t}:] ex V being a_neighborhood of A ex W being a_neighborhood of t st [:V,W:] c= G
proof
let Y, X be non empty TopSpace; ::_thesis: for t being Point of Y
for A being Subset of X st A is compact holds
for G being a_neighborhood of [:A,{t}:] ex V being a_neighborhood of A ex W being a_neighborhood of t st [:V,W:] c= G
let t be Point of Y; ::_thesis: for A being Subset of X st A is compact holds
for G being a_neighborhood of [:A,{t}:] ex V being a_neighborhood of A ex W being a_neighborhood of t st [:V,W:] c= G
let A be Subset of X; ::_thesis: ( A is compact implies for G being a_neighborhood of [:A,{t}:] ex V being a_neighborhood of A ex W being a_neighborhood of t st [:V,W:] c= G )
assume A1: A is compact ; ::_thesis: for G being a_neighborhood of [:A,{t}:] ex V being a_neighborhood of A ex W being a_neighborhood of t st [:V,W:] c= G
let G be a_neighborhood of [:A,{t}:]; ::_thesis: ex V being a_neighborhood of A ex W being a_neighborhood of t st [:V,W:] c= G
A2: the carrier of [:X,Y:] = [: the carrier of X, the carrier of Y:] by Def2;
now__::_thesis:_ex_V_being_a_neighborhood_of_A_ex_W_being_a_neighborhood_of_t_st_[:V,W:]_c=_G
percases ( A <> {} X or A = {} X ) ;
supposeA3: A <> {} X ; ::_thesis: ex V being a_neighborhood of A ex W being a_neighborhood of t st [:V,W:] c= G
 [:A,{t}:] c= Int G by CONNSP_2:def_2;
then  [:A,{t}:] c= union (Base-Appr G) by Th14;
then  Base-Appr G is Cover of [:A,{t}:] by SETFAM_1:def_11;
then consider K being Subset-Family of [:X,Y:] such that
A4: K c= Base-Appr G and
A5: K is Cover of [:A,{t}:] and
A6: for c being set st c in K holds
c meets [:A,{t}:] by Th22;
reconsider PK = (Pr1 (X,Y)) .: K as Subset-Family of X ;
 K is open by A4, TOPS_2:11;
then A7: (Pr1 (X,Y)) .: K is open by Th19;
 PK is Cover of A by A5, Th21;
then consider M being Subset-Family of X such that
A8: M c= (Pr1 (X,Y)) .: K and
A9: M is Cover of A and
A10: M is finite by A1, A7, COMPTS_1:def_4;
consider N being Subset-Family of [:X,Y:] such that
A11: N c= K and
A12: N is finite and
A13: (Pr1 (X,Y)) .: N = M by A8, A10, Th23;
reconsider F = (Pr1 (X,Y)) .: N as Subset-Family of X ;
A14: N is Cover of [:A,{t}:]
proof
let e1, e2 be set ; :: according to RELAT_1:def_3,SETFAM_1:def_11 ::_thesis: ( not [e1,e2] in [:A,{t}:] or [e1,e2] in union N )
A15: A c= union M by A9, SETFAM_1:def_11;
assume A16: [e1,e2] in [:A,{t}:] ; ::_thesis: [e1,e2] in union N
then  [e1,e2] `2 in {t} by MCART_1:10;
then  [e1,e2] `2 = t by TARSKI:def_1;
then A17: [e1,e2] = [([e1,e2] `1),t] ;
 [e1,e2] `1 in A by A16, MCART_1:10;
then consider X1 being set  such that
A18: [e1,e2] `1 in X1 and
A19: X1 in M by A15, TARSKI:def_4;
consider XY being Subset of [:X,Y:] such that
A20: XY in N and
A21: (Pr1 (X,Y)) . XY = X1 by A13, A19, FUNCT_2:65;
 XY in K by A11, A20;
then  XY in Base-Appr G by A4;
then consider X2 being Subset of X, Y2 being Subset of Y such that
A22: XY = [:X2,Y2:] and
 [:X2,Y2:] c= G and
 X2 is open and
 Y2 is open ;
 XY meets [:A,{t}:] by A6, A11, A20;
then consider xy being set  such that
A23: xy in XY and
A24: xy in [:A,{t}:] by XBOOLE_0:3;
 xy `2 in {t} by A24, MCART_1:10;
then  xy `2 = t by TARSKI:def_1;
then A25: t in Y2 by A22, A23, MCART_1:10;
 XY <> {} by A18, A21, FUNCT_3:8;
then  [e1,e2] `1 in X2 by A18, A21, A22, EQREL_1:50;
then  [e1,e2] in [:X2,Y2:] by A25, A17, ZFMISC_1:87;
hence  [e1,e2] in union N by A20, A22, TARSKI:def_4; ::_thesis: verum
end;
then  F is Cover of A by Th21;
then A26: A c= union F by SETFAM_1:def_11;
reconsider H = (Pr2 (X,Y)) .: N as Subset-Family of Y ;
A27: now__::_thesis:_for_C_being_set_st_C_in_H_holds_
t_in_C
let C be set ; ::_thesis: ( C in H implies t in C )
assume  C in H ; ::_thesis: t in C
then consider D being Subset of [:X,Y:] such that
A28: D in N and
A29: C = (pr2 ( the carrier of X, the carrier of Y)) .: D by Th17;
 D meets [:A,{t}:] by A6, A11, A28;
then  D /\ [:A,{t}:] <> {} by XBOOLE_0:def_7;
then consider x being Point of [:X,Y:] such that
A30: x in D /\ [:A,{t}:] by SUBSET_1:4;
A31: x in [:A,{t}:] by A30, XBOOLE_0:def_4;
then  x `1 in A by MCART_1:10;
then A32: (pr2 ( the carrier of X, the carrier of Y)) . ((x `1),t) = t by FUNCT_3:def_5;
 x `2 in {t} by A31, MCART_1:10;
then  x `2 = t by TARSKI:def_1;
then A33: x = [(x `1),t] by A2, MCART_1:21;
 x in D by A30, XBOOLE_0:def_4;
hence  t in C by A2, A29, A33, A32, FUNCT_2:35; ::_thesis: verum
end;
 [:A,{t}:] c= union N by A14, SETFAM_1:def_11;
then  N <> {} by A3, ZFMISC_1:2;
then  H <> {} by Th20;
then A34: t in meet H by A27, SETFAM_1:def_1;
A35: N c= Base-Appr G by A4, A11, XBOOLE_1:1;
then A36: N is open by TOPS_2:11;
then  meet H is open by A12, Th19, TOPS_2:20;
then  t in Int (meet H) by A34, TOPS_1:23;
then reconsider W = meet H as a_neighborhood of t by CONNSP_2:def_1;
 union F is open by A36, Th19, TOPS_2:19;
then  A c= Int (union F) by A26, TOPS_1:23;
then reconsider V = union F as a_neighborhood of A by CONNSP_2:def_2;
take V = V; ::_thesis: ex W being a_neighborhood of t st [:V,W:] c= G
take W = W; ::_thesis: [:V,W:] c= G
now__::_thesis:_for_e_being_set_st_e_in_N_holds_
(_e_c=_G_&_ex_X1_being_Subset_of_X_ex_Y1_being_Subset_of_Y_st_e_=_[:X1,Y1:]_)
let e be set ; ::_thesis: ( e in N implies ( e c= G & ex X1 being Subset of X ex Y1 being Subset of Y st e = [:X1,Y1:] ) )
assume  e in N ; ::_thesis: ( e c= G & ex X1 being Subset of X ex Y1 being Subset of Y st e = [:X1,Y1:] )
then  e in Base-Appr G by A35;
then  ex X1 being Subset of X ex Y1 being Subset of Y st
( e = [:X1,Y1:] & [:X1,Y1:] c= G & X1 is open & Y1 is open ) ;
hence  ( e c= G & ex X1 being Subset of X ex Y1 being Subset of Y st e = [:X1,Y1:] ) ; ::_thesis: verum
end;
hence  [:V,W:] c= G by Th15; ::_thesis: verum
end;
suppose A = {} X ; ::_thesis: ex V being a_neighborhood of A ex W being a_neighborhood of t st [:V,W:] c= G
then  A c= Int ({} X) ;
then reconsider V = {} X as a_neighborhood of A by CONNSP_2:def_2;
set W = the a_neighborhood of t;
take V = V; ::_thesis: ex W being a_neighborhood of t st [:V,W:] c= G
take W = the a_neighborhood of t; ::_thesis: [:V,W:] c= G
 [:V,W:] = {} ;
hence  [:V,W:] c= G by XBOOLE_1:2; ::_thesis: verum
end;
end;
end;
hence  ex V being a_neighborhood of A ex W being a_neighborhood of t st [:V,W:] c= G ; ::_thesis: verum
end;

begin

definition
let X be 1-sorted ;
func TrivDecomp X ->  a_partition of the carrier of X equals :: BORSUK_1:def 6
 Class (id the carrier of X);
coherence
 Class (id the carrier of X) is a_partition of the carrier of X ;
end;

:: deftheorem  defines TrivDecomp BORSUK_1:def_6_:_
 for X being 1-sorted holds TrivDecomp X = Class (id the carrier of X);

registration
let X be non empty 1-sorted ;
cluster TrivDecomp X ->  non empty ;
coherence
 not TrivDecomp X is empty ;
end;

theorem Th26: :: BORSUK_1:26
for X being non empty TopSpace
for A being Subset of X st A in TrivDecomp X holds
ex x being Point of X st A = {x}
proof
let X be non empty TopSpace; ::_thesis: for A being Subset of X st A in TrivDecomp X holds
ex x being Point of X st A = {x}
let A be Subset of X; ::_thesis: ( A in TrivDecomp X implies ex x being Point of X st A = {x} )
assume  A in TrivDecomp X ; ::_thesis: ex x being Point of X st A = {x}
then consider x being set  such that
A1: x in the carrier of X and
A2: A = Class ((id the carrier of X),x) by EQREL_1:def_3;
reconsider x = x as Point of X by A1;
take  x ; ::_thesis: A = {x}
thus  A = {x} by A2, EQREL_1:25; ::_thesis: verum
end;

Lm1:  for X being non empty TopSpace
for A being Subset of X
for V being a_neighborhood of A ex W being Subset of X st
( W is open & A c= W & W c= V & ( for B being Subset of X st B in TrivDecomp X & B meets W holds
B c= W ) )
proof
let X be non empty TopSpace; ::_thesis: for A being Subset of X
for V being a_neighborhood of A ex W being Subset of X st
( W is open & A c= W & W c= V & ( for B being Subset of X st B in TrivDecomp X & B meets W holds
B c= W ) )
let A be Subset of X; ::_thesis: for V being a_neighborhood of A ex W being Subset of X st
( W is open & A c= W & W c= V & ( for B being Subset of X st B in TrivDecomp X & B meets W holds
B c= W ) )
let V be a_neighborhood of A; ::_thesis: ex W being Subset of X st
( W is open & A c= W & W c= V & ( for B being Subset of X st B in TrivDecomp X & B meets W holds
B c= W ) )
take  Int V ; ::_thesis: ( Int V is open & A c= Int V & Int V c= V & ( for B being Subset of X st B in TrivDecomp X & B meets Int V holds
B c= Int V ) )
thus  Int V is open ; ::_thesis: ( A c= Int V & Int V c= V & ( for B being Subset of X st B in TrivDecomp X & B meets Int V holds
B c= Int V ) )
thus  A c= Int V by CONNSP_2:def_2; ::_thesis: ( Int V c= V & ( for B being Subset of X st B in TrivDecomp X & B meets Int V holds
B c= Int V ) )
thus  Int V c= V by TOPS_1:16; ::_thesis: for B being Subset of X st B in TrivDecomp X & B meets Int V holds
B c= Int V
let B be Subset of X; ::_thesis: ( B in TrivDecomp X & B meets Int V implies B c= Int V )
assume that
A1: B in TrivDecomp X and
A2: B meets Int V ; ::_thesis: B c= Int V
consider x being Point of X such that
A3: B = {x} by A1, Th26;
 x in Int V by A2, A3, ZFMISC_1:50;
hence  B c= Int V by A3, ZFMISC_1:31; ::_thesis: verum
end;

definition
let X be TopSpace;
let D be a_partition of the carrier of X;
func space D ->  strict TopSpace means :Def7: :: BORSUK_1:def 7
( the carrier of it = D & the topology of it =  {  A where A is Subset of D : union A in the topology of X  }  );
existence
 ex b1 being strict TopSpace st
( the carrier of b1 = D & the topology of b1 =  {  A where A is Subset of D : union A in the topology of X  }  )
proof
set t =  {  A where A is Subset of D : union A in the topology of X  }  ;
  {  A where A is Subset of D : union A in the topology of X  }  c= bool D
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in  {  A where A is Subset of D : union A in the topology of X  }  or e in bool D )
assume  e in  {  A where A is Subset of D : union A in the topology of X  }  ; ::_thesis: e in bool D
then  ex A being Subset of D st
( e = A & union A in the topology of X ) ;
hence  e in bool D ; ::_thesis: verum
end;
then reconsider t =  {  A where A is Subset of D : union A in the topology of X  }  as Subset-Family of D ;
set T = TopStruct(# D,t #);
 TopStruct(# D,t #) is TopSpace-like
proof
 union D = the carrier of X by EQREL_1:def_4;
then  ( D c= D & union D in the topology of X ) by PRE_TOPC:def_1;
hence  the carrier of TopStruct(# D,t #) in the topology of TopStruct(# D,t #) ; :: according to PRE_TOPC:def_1 ::_thesis: ( ( for b1 being Element of bool (bool the carrier of TopStruct(# D,t #)) holds
( not b1 c= the topology of TopStruct(# D,t #) or union b1 in the topology of TopStruct(# D,t #) ) ) & ( for b1, b2 being Element of bool the carrier of TopStruct(# D,t #) holds
( not b1 in the topology of TopStruct(# D,t #) or not b2 in the topology of TopStruct(# D,t #) or b1 /\ b2 in the topology of TopStruct(# D,t #) ) ) )
thus  for a being Subset-Family of TopStruct(# D,t #) st a c= the topology of TopStruct(# D,t #) holds
union a in the topology of TopStruct(# D,t #) ::_thesis: for b1, b2 being Element of bool the carrier of TopStruct(# D,t #) holds
( not b1 in the topology of TopStruct(# D,t #) or not b2 in the topology of TopStruct(# D,t #) or b1 /\ b2 in the topology of TopStruct(# D,t #) )
proof
let a be Subset-Family of TopStruct(# D,t #); ::_thesis: ( a c= the topology of TopStruct(# D,t #) implies union a in the topology of TopStruct(# D,t #) )
A1:  {  (union A) where A is Subset of TopStruct(# D,t #) : A in a  }  c= bool the carrier of X
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in  {  (union A) where A is Subset of TopStruct(# D,t #) : A in a  }  or e in bool the carrier of X )
assume  e in  {  (union A) where A is Subset of TopStruct(# D,t #) : A in a  }  ; ::_thesis: e in bool the carrier of X
then consider A being Subset of TopStruct(# D,t #) such that
A2: e = union A and
 A in a ;
 e c= the carrier of X
proof
let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in e or u in the carrier of X )
assume  u in e ; ::_thesis: u in the carrier of X
then consider x being set  such that
A3: u in x and
A4: x in A by A2, TARSKI:def_4;
 x in the carrier of TopStruct(# D,t #) by A4;
hence  u in the carrier of X by A3; ::_thesis: verum
end;
hence  e in bool the carrier of X ; ::_thesis: verum
end;
assume A5: a c= the topology of TopStruct(# D,t #) ; ::_thesis: union a in the topology of TopStruct(# D,t #)
  {  (union A) where A is Subset of TopStruct(# D,t #) : A in a  }  c= the topology of X
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in  {  (union A) where A is Subset of TopStruct(# D,t #) : A in a  }  or e in the topology of X )
assume  e in  {  (union A) where A is Subset of TopStruct(# D,t #) : A in a  }  ; ::_thesis: e in the topology of X
then consider A being Subset of TopStruct(# D,t #) such that
A6: e = union A and
A7: A in a ;
 A in the topology of TopStruct(# D,t #) by A5, A7;
then  ex B being Subset of D st
( A = B & union B in the topology of X ) ;
hence  e in the topology of X by A6; ::_thesis: verum
end;
then  union  {  (union A) where A is Subset of TopStruct(# D,t #) : A in a  }  in the topology of X by A1, PRE_TOPC:def_1;
then  union (union a) in the topology of X by EQREL_1:54;
hence  union a in the topology of TopStruct(# D,t #) ; ::_thesis: verum
end;
let a, b be Subset of TopStruct(# D,t #); ::_thesis: ( not a in the topology of TopStruct(# D,t #) or not b in the topology of TopStruct(# D,t #) or a /\ b in the topology of TopStruct(# D,t #) )
assume that
A8: a in the topology of TopStruct(# D,t #) and
A9: b in the topology of TopStruct(# D,t #) ; ::_thesis: a /\ b in the topology of TopStruct(# D,t #)
consider B being Subset of D such that
A10: b = B and
A11: union B in the topology of X by A9;
consider A being Subset of D such that
A12: a = A and
A13: union A in the topology of X by A8;
 union (A /\ B) = (union A) /\ (union B) by EQREL_1:62;
then  union (A /\ B) in the topology of X by A13, A11, PRE_TOPC:def_1;
hence  a /\ b in the topology of TopStruct(# D,t #) by A12, A10; ::_thesis: verum
end;
then reconsider T = TopStruct(# D,t #) as strict TopSpace ;
take  T ; ::_thesis: ( the carrier of T = D & the topology of T =  {  A where A is Subset of D : union A in the topology of X  }  )
thus  ( the carrier of T = D & the topology of T =  {  A where A is Subset of D : union A in the topology of X  }  ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being strict TopSpace st the carrier of b1 = D & the topology of b1 =  {  A where A is Subset of D : union A in the topology of X  }  & the carrier of b2 = D & the topology of b2 =  {  A where A is Subset of D : union A in the topology of X  }  holds
b1 = b2 ;
end;

:: deftheorem Def7 defines space BORSUK_1:def_7_:_
 for X being TopSpace
for D being a_partition of the carrier of X
for b3 being strict TopSpace holds
( b3 = space D iff ( the carrier of b3 = D & the topology of b3 =  {  A where A is Subset of D : union A in the topology of X  }  ) );

registration
let X be non empty TopSpace;
let D be a_partition of the carrier of X;
cluster space D ->  non empty strict ;
coherence
 not space D is empty by Def7;
end;

theorem Th27: :: BORSUK_1:27
for X being non empty TopSpace
for D being non empty a_partition of the carrier of X
for A being Subset of D holds
( union A in the topology of X iff A in the topology of (space D) )
proof
let X be non empty TopSpace; ::_thesis: for D being non empty a_partition of the carrier of X
for A being Subset of D holds
( union A in the topology of X iff A in the topology of (space D) )
let D be non empty a_partition of the carrier of X; ::_thesis: for A being Subset of D holds
( union A in the topology of X iff A in the topology of (space D) )
let B be Subset of D; ::_thesis: ( union B in the topology of X iff B in the topology of (space D) )
A1: the topology of (space D) =  {  A where A is Subset of D : union A in the topology of X  }  by Def7;
hence  ( union B in the topology of X implies B in the topology of (space D) ) ; ::_thesis: ( B in the topology of (space D) implies union B in the topology of X )
assume  B in the topology of (space D) ; ::_thesis: union B in the topology of X
then  ex A being Subset of D st
( B = A & union A in the topology of X ) by A1;
hence  union B in the topology of X ; ::_thesis: verum
end;

definition
let X be non empty TopSpace;
let D be non empty a_partition of the carrier of X;
func Proj D ->  continuous Function of X,(space D) equals :: BORSUK_1:def 8
 proj D;
coherence
 proj D is continuous Function of X,(space D)
proof
reconsider F = proj D as Function of X,(space D) by Def7;
A1: the carrier of (space D) = D by Def7;
 F is continuous
proof
let W be Point of X; :: according to BORSUK_1:def_1 ::_thesis: for G being a_neighborhood of F . W ex H being a_neighborhood of W st F .: H c= G
let G be a_neighborhood of F . W; ::_thesis: ex H being a_neighborhood of W st F .: H c= G
reconsider H = union (Int G) as Subset of X by A1, EQREL_1:61;
 F . W in Int G by CONNSP_2:def_1;
then  W in F " (Int G) by FUNCT_2:38;
then A2: W in union (Int G) by A1, EQREL_1:67;
 Int G in the topology of (space D) by PRE_TOPC:def_2;
then  union (Int G) in the topology of X by A1, Th27;
then  H is open by PRE_TOPC:def_2;
then  W in Int H by A2, TOPS_1:23;
then  W in Int (F " (Int G)) by A1, EQREL_1:67;
then reconsider N = F " (Int G) as a_neighborhood of W by CONNSP_2:def_1;
take  N ; ::_thesis: F .: N c= G
 ( F .: N c= Int G & Int G c= G ) by FUNCT_1:75, TOPS_1:16;
hence  F .: N c= G by XBOOLE_1:1; ::_thesis: verum
end;
hence  proj D is continuous Function of X,(space D) ; ::_thesis: verum
end;
correctness
;
end;

:: deftheorem  defines Proj BORSUK_1:def_8_:_
 for X being non empty TopSpace
for D being non empty a_partition of the carrier of X holds Proj D = proj D;

theorem :: BORSUK_1:28
for X being non empty TopSpace
for D being non empty a_partition of the carrier of X
for W being Point of X holds W in (Proj D) . W by EQREL_1:def_9;

theorem Th29: :: BORSUK_1:29
for X being non empty TopSpace
for D being non empty a_partition of the carrier of X
for W being Point of (space D) ex W9 being Point of X st (Proj D) . W9 = W
proof
let X be non empty TopSpace; ::_thesis: for D being non empty a_partition of the carrier of X
for W being Point of (space D) ex W9 being Point of X st (Proj D) . W9 = W
let D be non empty a_partition of the carrier of X; ::_thesis: for W being Point of (space D) ex W9 being Point of X st (Proj D) . W9 = W
let W be Point of (space D); ::_thesis: ex W9 being Point of X st (Proj D) . W9 = W
reconsider p = W as Element of D by Def7;
consider W9 being Point of X such that
A1: (proj D) . W9 = p by EQREL_1:68;
take  W9 ; ::_thesis: (Proj D) . W9 = W
thus  (Proj D) . W9 = W by A1; ::_thesis: verum
end;

theorem Th30: :: BORSUK_1:30
for X being non empty TopSpace
for D being non empty a_partition of the carrier of X holds rng (Proj D) = the carrier of (space D)
proof
let X be non empty TopSpace; ::_thesis: for D being non empty a_partition of the carrier of X holds rng (Proj D) = the carrier of (space D)
let D be non empty a_partition of the carrier of X; ::_thesis: rng (Proj D) = the carrier of (space D)
thus  rng (Proj D) c= the carrier of (space D) ; :: according to XBOOLE_0:def_10 ::_thesis: the carrier of (space D) c= rng (Proj D)
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in the carrier of (space D) or e in rng (Proj D) )
assume  e in the carrier of (space D) ; ::_thesis: e in rng (Proj D)
then  ex p being Point of X st (Proj D) . p = e by Th29;
hence  e in rng (Proj D) by FUNCT_2:4; ::_thesis: verum
end;

definition
let XX be non empty TopSpace;
let X be non empty SubSpace of XX;
let D be non empty a_partition of the carrier of X;
func TrivExt D ->  non empty a_partition of the carrier of XX equals :: BORSUK_1:def 9
D \/  {  {p} where p is Point of XX : not p in the carrier of X  }  ;
coherence
 D \/  {  {p} where p is Point of XX : not p in the carrier of X  }  is non empty a_partition of the carrier of XX
proof
set E = D \/  {  {p} where p is Point of XX : not p in the carrier of X  }  ;
 D \/  {  {p} where p is Point of XX : not p in the carrier of X  }  c= bool the carrier of XX
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in D \/  {  {p} where p is Point of XX : not p in the carrier of X  }  or e in bool the carrier of XX )
assume A1: e in D \/  {  {p} where p is Point of XX : not p in the carrier of X  }  ; ::_thesis: e in bool the carrier of XX
now__::_thesis:_e_in_bool_the_carrier_of_XX
percases ( e in D or e in  {  {p} where p is Point of XX : not p in the carrier of X  }  ) by A1, XBOOLE_0:def_3;
supposeA2: e in D ; ::_thesis: e in bool the carrier of XX
 bool the carrier of X c= bool the carrier of XX by Th1, ZFMISC_1:67;
hence  e in bool the carrier of XX by A2, TARSKI:def_3; ::_thesis: verum
end;
suppose e in  {  {p} where p is Point of XX : not p in the carrier of X  }  ; ::_thesis: e in bool the carrier of XX
then  ex p being Point of XX st
( e = {p} & not p in the carrier of X ) ;
hence  e in bool the carrier of XX ; ::_thesis: verum
end;
end;
end;
hence  e in bool the carrier of XX ; ::_thesis: verum
end;
then reconsider E = D \/  {  {p} where p is Point of XX : not p in the carrier of X  }  as Subset-Family of XX ;
 E is a_partition of the carrier of XX
proof
now__::_thesis:_for_e_being_set_holds_
(_(_e_in_the_carrier_of_XX_\_the_carrier_of_X_implies_ex_Z_being_set_st_
(_e_in_Z_&_Z_in__{__{p}_where_p_is_Point_of_XX_:_not_p_in_the_carrier_of_X__}__)_)_&_(_ex_Z_being_set_st_
(_e_in_Z_&_Z_in__{__{p}_where_p_is_Point_of_XX_:_not_p_in_the_carrier_of_X__}__)_implies_e_in_the_carrier_of_XX_\_the_carrier_of_X_)_)
let e be set ; ::_thesis: ( ( e in the carrier of XX \ the carrier of X implies ex Z being set st
( e in Z & Z in  {  {p} where p is Point of XX : not p in the carrier of X  }  ) ) & ( ex Z being set st
( e in Z & Z in  {  {p} where p is Point of XX : not p in the carrier of X  }  ) implies e in the carrier of XX \ the carrier of X ) )
thus  ( e in the carrier of XX \ the carrier of X implies ex Z being set st
( e in Z & Z in  {  {p} where p is Point of XX : not p in the carrier of X  }  ) ) ::_thesis: ( ex Z being set st
( e in Z & Z in  {  {p} where p is Point of XX : not p in the carrier of X  }  ) implies e in the carrier of XX \ the carrier of X )
proof
assume A3: e in the carrier of XX \ the carrier of X ; ::_thesis: ex Z being set st
( e in Z & Z in  {  {p} where p is Point of XX : not p in the carrier of X  }  )
take  {e} ; ::_thesis: ( e in {e} & {e} in  {  {p} where p is Point of XX : not p in the carrier of X  }  )
thus  e in {e} by TARSKI:def_1; ::_thesis: {e} in  {  {p} where p is Point of XX : not p in the carrier of X  }
 not e in the carrier of X by A3, XBOOLE_0:def_5;
hence  {e} in  {  {p} where p is Point of XX : not p in the carrier of X  }  by A3; ::_thesis: verum
end;
given Z being set  such that A4: e in Z and
A5: Z in  {  {p} where p is Point of XX : not p in the carrier of X  }  ; ::_thesis: e in the carrier of XX \ the carrier of X
consider p being Point of XX such that
A6: Z = {p} and
A7: not p in the carrier of X by A5;
 e = p by A4, A6, TARSKI:def_1;
hence  e in the carrier of XX \ the carrier of X by A7, XBOOLE_0:def_5; ::_thesis: verum
end;
then A8: union  {  {p} where p is Point of XX : not p in the carrier of X  }  = the carrier of XX \ the carrier of X by TARSKI:def_4;
thus  union E = (union D) \/ (union  {  {p} where p is Point of XX : not p in the carrier of X  }  ) by ZFMISC_1:78
.= the carrier of X \/ ( the carrier of XX \ the carrier of X) by A8, EQREL_1:def_4
.= the carrier of XX by Th1, XBOOLE_1:45 ; :: according to EQREL_1:def_4 ::_thesis: for b1 being Element of bool the carrier of XX holds
( not b1 in E or ( not b1 = {} & ( for b2 being Element of bool the carrier of XX holds
( not b2 in E or b1 = b2 or b1 misses b2 ) ) ) )
let A be Subset of XX; ::_thesis: ( not A in E or ( not A = {} & ( for b1 being Element of bool the carrier of XX holds
( not b1 in E or A = b1 or A misses b1 ) ) ) )
assume A9: A in E ; ::_thesis: ( not A = {} & ( for b1 being Element of bool the carrier of XX holds
( not b1 in E or A = b1 or A misses b1 ) ) )
now__::_thesis:_A_<>_{}
percases ( A in D or A in  {  {p} where p is Point of XX : not p in the carrier of X  }  ) by A9, XBOOLE_0:def_3;
suppose A in D ; ::_thesis: A <> {}
hence  A <> {} by EQREL_1:def_4; ::_thesis: verum
end;
suppose A in  {  {p} where p is Point of XX : not p in the carrier of X  }  ; ::_thesis: A <> {}
then  ex p being Point of XX st
( A = {p} & not p in the carrier of X ) ;
hence  A <> {} ; ::_thesis: verum
end;
end;
end;
hence  A <> {} ; ::_thesis: for b1 being Element of bool the carrier of XX holds
( not b1 in E or A = b1 or A misses b1 )
let B be Subset of XX; ::_thesis: ( not B in E or A = B or A misses B )
assume A10: B in E ; ::_thesis: ( A = B or A misses B )
now__::_thesis:_(_A_=_B_or_A_misses_B_)
percases ( A in D or A in  {  {p} where p is Point of XX : not p in the carrier of X  }  ) by A9, XBOOLE_0:def_3;
supposeA11: A in D ; ::_thesis: ( A = B or A misses B )
now__::_thesis:_(_A_=_B_or_A_misses_B_)
percases ( B in D or B in  {  {p} where p is Point of XX : not p in the carrier of X  }  ) by A10, XBOOLE_0:def_3;
suppose B in D ; ::_thesis: ( A = B or A misses B )
hence  ( A = B or A misses B ) by A11, EQREL_1:def_4; ::_thesis: verum
end;
suppose B in  {  {p} where p is Point of XX : not p in the carrier of X  }  ; ::_thesis: ( A = B or A misses B )
then  ex p being Point of XX st
( B = {p} & not p in the carrier of X ) ;
then  B misses the carrier of X by ZFMISC_1:50;
hence  ( A = B or A misses B ) by A11, XBOOLE_1:63; ::_thesis: verum
end;
end;
end;
hence  ( A = B or A misses B ) ; ::_thesis: verum
end;
suppose A in  {  {p} where p is Point of XX : not p in the carrier of X  }  ; ::_thesis: ( A = B or A misses B )
then A12: ex p being Point of XX st
( A = {p} & not p in the carrier of X ) ;
then A13: A misses the carrier of X by ZFMISC_1:50;
now__::_thesis:_(_A_=_B_or_A_misses_B_)
percases ( B in D or B in  {  {p} where p is Point of XX : not p in the carrier of X  }  ) by A10, XBOOLE_0:def_3;
suppose B in D ; ::_thesis: ( A = B or A misses B )
hence  ( A = B or A misses B ) by A13, XBOOLE_1:63; ::_thesis: verum
end;
suppose B in  {  {p} where p is Point of XX : not p in the carrier of X  }  ; ::_thesis: ( A = B or A misses B )
then  ex p being Point of XX st
( B = {p} & not p in the carrier of X ) ;
hence  ( A = B or A misses B ) by A12, ZFMISC_1:11; ::_thesis: verum
end;
end;
end;
hence  ( A = B or A misses B ) ; ::_thesis: verum
end;
end;
end;
hence  ( A = B or A misses B ) ; ::_thesis: verum
end;
hence  D \/  {  {p} where p is Point of XX : not p in the carrier of X  }  is non empty a_partition of the carrier of XX ; ::_thesis: verum
end;
correctness
;
end;

:: deftheorem  defines TrivExt BORSUK_1:def_9_:_
 for XX being non empty TopSpace
for X being non empty SubSpace of XX
for D being non empty a_partition of the carrier of X holds TrivExt D = D \/  {  {p} where p is Point of XX : not p in the carrier of X  }  ;

theorem Th31: :: BORSUK_1:31
for XX being non empty TopSpace
for X being non empty SubSpace of XX
for D being non empty a_partition of the carrier of X
for A being Subset of XX holds
( not A in TrivExt D or A in D or ex x being Point of XX st
( not x in [#] X & A = {x} ) )
proof
let XX be non empty TopSpace; ::_thesis: for X being non empty SubSpace of XX
for D being non empty a_partition of the carrier of X
for A being Subset of XX holds
( not A in TrivExt D or A in D or ex x being Point of XX st
( not x in [#] X & A = {x} ) )
let X be non empty SubSpace of XX; ::_thesis: for D being non empty a_partition of the carrier of X
for A being Subset of XX holds
( not A in TrivExt D or A in D or ex x being Point of XX st
( not x in [#] X & A = {x} ) )
let D be non empty a_partition of the carrier of X; ::_thesis: for A being Subset of XX holds
( not A in TrivExt D or A in D or ex x being Point of XX st
( not x in [#] X & A = {x} ) )
let A be Subset of XX; ::_thesis: ( not A in TrivExt D or A in D or ex x being Point of XX st
( not x in [#] X & A = {x} ) )
assume A1: A in TrivExt D ; ::_thesis: ( A in D or ex x being Point of XX st
( not x in [#] X & A = {x} ) )
now__::_thesis:_(_(_A_in_D_&_A_in_D_)_or_(_A_in__{__{p}_where_p_is_Point_of_XX_:_not_p_in_the_carrier_of_X__}__&_ex_x_being_Point_of_XX_st_
(_not_x_in_[#]_X_&_A_=_{x}_)_)_)
percases ( A in D or A in  {  {p} where p is Point of XX : not p in the carrier of X  }  ) by A1, XBOOLE_0:def_3;
case A in D ; ::_thesis: A in D
hence  A in D ; ::_thesis: verum
end;
case A in  {  {p} where p is Point of XX : not p in the carrier of X  }  ; ::_thesis: ex x being Point of XX st
( not x in [#] X & A = {x} )
then consider x being Point of XX such that
A2: A = {x} and
A3: not x in the carrier of X ;
take x = x; ::_thesis: ( not x in [#] X & A = {x} )
thus  not x in [#] X by A3; ::_thesis: A = {x}
thus  A = {x} by A2; ::_thesis: verum
end;
end;
end;
hence  ( A in D or ex x being Point of XX st
( not x in [#] X & A = {x} ) ) ; ::_thesis: verum
end;

theorem Th32: :: BORSUK_1:32
for XX being non empty TopSpace
for X being non empty SubSpace of XX
for D being non empty a_partition of the carrier of X
for x being Point of XX st not x in the carrier of X holds
{x} in TrivExt D
proof
let XX be non empty TopSpace; ::_thesis: for X being non empty SubSpace of XX
for D being non empty a_partition of the carrier of X
for x being Point of XX st not x in the carrier of X holds
{x} in TrivExt D
let X be non empty SubSpace of XX; ::_thesis: for D being non empty a_partition of the carrier of X
for x being Point of XX st not x in the carrier of X holds
{x} in TrivExt D
let D be non empty a_partition of the carrier of X; ::_thesis: for x being Point of XX st not x in the carrier of X holds
{x} in TrivExt D
let x be Point of XX; ::_thesis: ( not x in the carrier of X implies {x} in TrivExt D )
 union (TrivExt D) = the carrier of XX by EQREL_1:def_4;
then consider A being set  such that
A1: x in A and
A2: A in TrivExt D by TARSKI:def_4;
assume  not x in the carrier of X ; ::_thesis: {x} in TrivExt D
then  not A in D by A1;
then  A in  {  {p} where p is Point of XX : not p in the carrier of X  }  by A2, XBOOLE_0:def_3;
then  ex p being Point of XX st
( A = {p} & not p in the carrier of X ) ;
hence  {x} in TrivExt D by A1, A2, TARSKI:def_1; ::_thesis: verum
end;

theorem Th33: :: BORSUK_1:33
for XX being non empty TopSpace
for X being non empty SubSpace of XX
for D being non empty a_partition of the carrier of X
for W being Point of XX st W in the carrier of X holds
(Proj (TrivExt D)) . W = (Proj D) . W
proof
let XX be non empty TopSpace; ::_thesis: for X being non empty SubSpace of XX
for D being non empty a_partition of the carrier of X
for W being Point of XX st W in the carrier of X holds
(Proj (TrivExt D)) . W = (Proj D) . W
let X be non empty SubSpace of XX; ::_thesis: for D being non empty a_partition of the carrier of X
for W being Point of XX st W in the carrier of X holds
(Proj (TrivExt D)) . W = (Proj D) . W
let D be non empty a_partition of the carrier of X; ::_thesis: for W being Point of XX st W in the carrier of X holds
(Proj (TrivExt D)) . W = (Proj D) . W
let W be Point of XX; ::_thesis: ( W in the carrier of X implies (Proj (TrivExt D)) . W = (Proj D) . W )
assume A1: W in the carrier of X ; ::_thesis: (Proj (TrivExt D)) . W = (Proj D) . W
then reconsider p = W as Point of X ;
 ( D c= TrivExt D & (proj D) . p in D ) by XBOOLE_1:7;
then reconsider A = (Proj D) . W as Element of TrivExt D ;
 W in A by A1, EQREL_1:def_9;
hence  (Proj (TrivExt D)) . W = (Proj D) . W by EQREL_1:65; ::_thesis: verum
end;

theorem Th34: :: BORSUK_1:34
for XX being non empty TopSpace
for X being non empty SubSpace of XX
for D being non empty a_partition of the carrier of X
for W being Point of XX st not W in the carrier of X holds
(Proj (TrivExt D)) . W = {W}
proof
let XX be non empty TopSpace; ::_thesis: for X being non empty SubSpace of XX
for D being non empty a_partition of the carrier of X
for W being Point of XX st not W in the carrier of X holds
(Proj (TrivExt D)) . W = {W}
let X be non empty SubSpace of XX; ::_thesis: for D being non empty a_partition of the carrier of X
for W being Point of XX st not W in the carrier of X holds
(Proj (TrivExt D)) . W = {W}
let D be non empty a_partition of the carrier of X; ::_thesis: for W being Point of XX st not W in the carrier of X holds
(Proj (TrivExt D)) . W = {W}
let W be Point of XX; ::_thesis: ( not W in the carrier of X implies (Proj (TrivExt D)) . W = {W} )
assume  not W in the carrier of X ; ::_thesis: (Proj (TrivExt D)) . W = {W}
then  ( W in {W} & {W} in TrivExt D ) by Th32, TARSKI:def_1;
hence  (Proj (TrivExt D)) . W = {W} by EQREL_1:65; ::_thesis: verum
end;

theorem Th35: :: BORSUK_1:35
for XX being non empty TopSpace
for X being non empty SubSpace of XX
for D being non empty a_partition of the carrier of X
for W, W9 being Point of XX st not W in the carrier of X & (Proj (TrivExt D)) . W = (Proj (TrivExt D)) . W9 holds
W = W9
proof
let XX be non empty TopSpace; ::_thesis: for X being non empty SubSpace of XX
for D being non empty a_partition of the carrier of X
for W, W9 being Point of XX st not W in the carrier of X & (Proj (TrivExt D)) . W = (Proj (TrivExt D)) . W9 holds
W = W9
let X be non empty SubSpace of XX; ::_thesis: for D being non empty a_partition of the carrier of X
for W, W9 being Point of XX st not W in the carrier of X & (Proj (TrivExt D)) . W = (Proj (TrivExt D)) . W9 holds
W = W9
let D be non empty a_partition of the carrier of X; ::_thesis: for W, W9 being Point of XX st not W in the carrier of X & (Proj (TrivExt D)) . W = (Proj (TrivExt D)) . W9 holds
W = W9
let W, W9 be Point of XX; ::_thesis: ( not W in the carrier of X & (Proj (TrivExt D)) . W = (Proj (TrivExt D)) . W9 implies W = W9 )
assume  not W in the carrier of X ; ::_thesis: ( not (Proj (TrivExt D)) . W = (Proj (TrivExt D)) . W9 or W = W9 )
then A1: (Proj (TrivExt D)) . W = {W} by Th34;
 W9 in (Proj (TrivExt D)) . W9 by EQREL_1:def_9;
hence  ( not (Proj (TrivExt D)) . W = (Proj (TrivExt D)) . W9 or W = W9 ) by A1, TARSKI:def_1; ::_thesis: verum
end;

theorem Th36: :: BORSUK_1:36
for XX being non empty TopSpace
for X being non empty SubSpace of XX
for D being non empty a_partition of the carrier of X
for e being Point of XX st (Proj (TrivExt D)) . e in the carrier of (space D) holds
e in the carrier of X
proof
let XX be non empty TopSpace; ::_thesis: for X being non empty SubSpace of XX
for D being non empty a_partition of the carrier of X
for e being Point of XX st (Proj (TrivExt D)) . e in the carrier of (space D) holds
e in the carrier of X
let X be non empty SubSpace of XX; ::_thesis: for D being non empty a_partition of the carrier of X
for e being Point of XX st (Proj (TrivExt D)) . e in the carrier of (space D) holds
e in the carrier of X
let D be non empty a_partition of the carrier of X; ::_thesis: for e being Point of XX st (Proj (TrivExt D)) . e in the carrier of (space D) holds
e in the carrier of X
let e be Point of XX; ::_thesis: ( (Proj (TrivExt D)) . e in the carrier of (space D) implies e in the carrier of X )
assume  (Proj (TrivExt D)) . e in the carrier of (space D) ; ::_thesis: e in the carrier of X
then A1: (Proj (TrivExt D)) . e in D by Def7;
 e in (Proj (TrivExt D)) . e by EQREL_1:def_9;
hence  e in the carrier of X by A1; ::_thesis: verum
end;

theorem Th37: :: BORSUK_1:37
for XX being non empty TopSpace
for X being non empty SubSpace of XX
for D being non empty a_partition of the carrier of X
for e being set st e in the carrier of X holds
(Proj (TrivExt D)) . e in the carrier of (space D)
proof
let XX be non empty TopSpace; ::_thesis: for X being non empty SubSpace of XX
for D being non empty a_partition of the carrier of X
for e being set st e in the carrier of X holds
(Proj (TrivExt D)) . e in the carrier of (space D)
let X be non empty SubSpace of XX; ::_thesis: for D being non empty a_partition of the carrier of X
for e being set st e in the carrier of X holds
(Proj (TrivExt D)) . e in the carrier of (space D)
let D be non empty a_partition of the carrier of X; ::_thesis: for e being set st e in the carrier of X holds
(Proj (TrivExt D)) . e in the carrier of (space D)
let e be set ; ::_thesis: ( e in the carrier of X implies (Proj (TrivExt D)) . e in the carrier of (space D) )
assume A1: e in the carrier of X ; ::_thesis: (Proj (TrivExt D)) . e in the carrier of (space D)
then reconsider x = e as Point of X ;
 the carrier of X c= the carrier of XX by Th1;
then  (Proj D) . x = (Proj (TrivExt D)) . x by A1, Th33;
hence  (Proj (TrivExt D)) . e in the carrier of (space D) ; ::_thesis: verum
end;

begin

definition
let X be non empty TopSpace;
mode u.s.c._decomposition of X ->  non empty a_partition of the carrier of X means :Def10: :: BORSUK_1:def 10
 for A being Subset of X st A in it holds
for V being a_neighborhood of A ex W being Subset of X st
( W is open & A c= W & W c= V & ( for B being Subset of X st B in it & B meets W holds
B c= W ) );
correctness
existence
ex b1 being non empty a_partition of the carrier of X st
for A being Subset of X st A in b1 holds
for V being a_neighborhood of A ex W being Subset of X st
( W is open & A c= W & W c= V & ( for B being Subset of X st B in b1 & B meets W holds
B c= W ) );
proof
take  TrivDecomp X ; ::_thesis: for A being Subset of X st A in TrivDecomp X holds
for V being a_neighborhood of A ex W being Subset of X st
( W is open & A c= W & W c= V & ( for B being Subset of X st B in TrivDecomp X & B meets W holds
B c= W ) )
thus  for A being Subset of X st A in TrivDecomp X holds
for V being a_neighborhood of A ex W being Subset of X st
( W is open & A c= W & W c= V & ( for B being Subset of X st B in TrivDecomp X & B meets W holds
B c= W ) ) by Lm1; ::_thesis: verum
end;
end;

:: deftheorem Def10 defines u.s.c._decomposition BORSUK_1:def_10_:_
 for X being non empty TopSpace
for b2 being non empty a_partition of the carrier of X holds
( b2 is u.s.c._decomposition of X iff for A being Subset of X st A in b2 holds
for V being a_neighborhood of A ex W being Subset of X st
( W is open & A c= W & W c= V & ( for B being Subset of X st B in b2 & B meets W holds
B c= W ) ) );

theorem Th38: :: BORSUK_1:38
for X being non empty TopSpace
for D being u.s.c._decomposition of X
for t being Point of (space D)
for G being a_neighborhood of (Proj D) " {t} holds (Proj D) .: G is a_neighborhood of t
proof
let X be non empty TopSpace; ::_thesis: for D being u.s.c._decomposition of X
for t being Point of (space D)
for G being a_neighborhood of (Proj D) " {t} holds (Proj D) .: G is a_neighborhood of t
let D be u.s.c._decomposition of X; ::_thesis: for t being Point of (space D)
for G being a_neighborhood of (Proj D) " {t} holds (Proj D) .: G is a_neighborhood of t
let t be Point of (space D); ::_thesis: for G being a_neighborhood of (Proj D) " {t} holds (Proj D) .: G is a_neighborhood of t
let G be a_neighborhood of (Proj D) " {t}; ::_thesis: (Proj D) .: G is a_neighborhood of t
A1: the carrier of (space D) = D by Def7;
then  (Proj D) " {t} = t by EQREL_1:66;
then consider W being Subset of X such that
A2: W is open and
A3: (Proj D) " {t} c= W and
A4: W c= G and
A5: for B being Subset of X st B in D & B meets W holds
B c= W by A1, Def10;
set Q = (Proj D) .: W;
A6: (Proj D) .: ((Proj D) " {t}) c= (Proj D) .: W by A3, RELAT_1:123;
union ((Proj D) .: W) = (proj D) " ((Proj D) .: W) by A1, EQREL_1:67
.= W by A5, EQREL_1:69 ;
then  union ((Proj D) .: W) in the topology of X by A2, PRE_TOPC:def_2;
then  (Proj D) .: W in the topology of (space D) by A1, Th27;
then A7: (Proj D) .: W is open by PRE_TOPC:def_2;
 rng (Proj D) = the carrier of (space D) by Th30;
then  {t} c= (Proj D) .: W by A6, FUNCT_1:77;
then A8: t in (Proj D) .: W by ZFMISC_1:31;
 (Proj D) .: W c= (Proj D) .: G by A4, RELAT_1:123;
then  t in Int ((Proj D) .: G) by A7, A8, TOPS_1:22;
hence  (Proj D) .: G is a_neighborhood of t by CONNSP_2:def_1; ::_thesis: verum
end;

theorem Th39: :: BORSUK_1:39
for X being non empty TopSpace holds TrivDecomp X is u.s.c._decomposition of X
proof
let X be non empty TopSpace; ::_thesis: TrivDecomp X is u.s.c._decomposition of X
thus  for A being Subset of X st A in TrivDecomp X holds
for V being a_neighborhood of A ex W being Subset of X st
( W is open & A c= W & W c= V & ( for B being Subset of X st B in TrivDecomp X & B meets W holds
B c= W ) ) by Lm1; :: according to BORSUK_1:def_10 ::_thesis: verum
end;

definition
let X be TopSpace;
let IT be SubSpace of X;
attrIT is closed  means :Def11: :: BORSUK_1:def 11
 for A being Subset of X st A = the carrier of IT holds
A is closed ;
end;

:: deftheorem Def11 defines closed BORSUK_1:def_11_:_
 for X being TopSpace
for IT being SubSpace of X holds
( IT is closed iff for A being Subset of X st A = the carrier of IT holds
A is closed );

Lm2:  for T being TopStruct holds TopStruct(# the carrier of T, the topology of T #) is SubSpace of T
proof
let T be TopStruct ; ::_thesis: TopStruct(# the carrier of T, the topology of T #) is SubSpace of T
set S = TopStruct(# the carrier of T, the topology of T #);
thus  [#] TopStruct(# the carrier of T, the topology of T #) c= [#] T ; :: according to PRE_TOPC:def_4 ::_thesis: for b1 being Element of bool the carrier of TopStruct(# the carrier of T, the topology of T #) holds
( ( not b1 in the topology of TopStruct(# the carrier of T, the topology of T #) or ex b2 being Element of bool the carrier of T st
( b2 in the topology of T & b1 = b2 /\ ([#] TopStruct(# the carrier of T, the topology of T #)) ) ) & ( for b2 being Element of bool the carrier of T holds
( not b2 in the topology of T or not b1 = b2 /\ ([#] TopStruct(# the carrier of T, the topology of T #)) ) or b1 in the topology of TopStruct(# the carrier of T, the topology of T #) ) )
let P be Subset of TopStruct(# the carrier of T, the topology of T #); ::_thesis: ( ( not P in the topology of TopStruct(# the carrier of T, the topology of T #) or ex b1 being Element of bool the carrier of T st
( b1 in the topology of T & P = b1 /\ ([#] TopStruct(# the carrier of T, the topology of T #)) ) ) & ( for b1 being Element of bool the carrier of T holds
( not b1 in the topology of T or not P = b1 /\ ([#] TopStruct(# the carrier of T, the topology of T #)) ) or P in the topology of TopStruct(# the carrier of T, the topology of T #) ) )
hereby  ::_thesis: ( for b1 being Element of bool the carrier of T holds
( not b1 in the topology of T or not P = b1 /\ ([#] TopStruct(# the carrier of T, the topology of T #)) ) or P in the topology of TopStruct(# the carrier of T, the topology of T #) )
reconsider Q = P as Subset of T ;
assume A1: P in the topology of TopStruct(# the carrier of T, the topology of T #) ; ::_thesis: ex Q being Subset of T st
( Q in the topology of T & P = Q /\ ([#] TopStruct(# the carrier of T, the topology of T #)) )
take Q = Q; ::_thesis: ( Q in the topology of T & P = Q /\ ([#] TopStruct(# the carrier of T, the topology of T #)) )
thus  Q in the topology of T by A1; ::_thesis: P = Q /\ ([#] TopStruct(# the carrier of T, the topology of T #))
thus  P = Q /\ ([#] TopStruct(# the carrier of T, the topology of T #)) by XBOOLE_1:28; ::_thesis: verum
end;
given Q being Subset of T such that A2: ( Q in the topology of T & P = Q /\ ([#] TopStruct(# the carrier of T, the topology of T #)) ) ; ::_thesis: P in the topology of TopStruct(# the carrier of T, the topology of T #)
thus  P in the topology of TopStruct(# the carrier of T, the topology of T #) by A2, XBOOLE_1:28; ::_thesis: verum
end;

registration
let X be TopSpace;
cluster strict TopSpace-like closed for SubSpace of X;
existence
 ex b1 being SubSpace of X st
( b1 is strict & b1 is closed )
proof
reconsider Y = TopStruct(# the carrier of X, the topology of X #) as strict SubSpace of X by Lm2;
take  Y ; ::_thesis: ( Y is strict & Y is closed )
 Y is closed
proof
let A be Subset of X; :: according to BORSUK_1:def_11 ::_thesis: ( A = the carrier of Y implies A is closed )
assume  A = the carrier of Y ; ::_thesis: A is closed
then  A = [#] X ;
hence  A is closed ; ::_thesis: verum
end;
hence  ( Y is strict & Y is closed ) ; ::_thesis: verum
end;
end;

registration
let X be non empty TopSpace;
cluster non empty strict TopSpace-like closed for SubSpace of X;
existence
 ex b1 being SubSpace of X st
( b1 is strict & b1 is closed & not b1 is empty )
proof
 X | ([#] X) is closed
proof
let A be Subset of X; :: according to BORSUK_1:def_11 ::_thesis: ( A = the carrier of (X | ([#] X)) implies A is closed )
assume  A = the carrier of (X | ([#] X)) ; ::_thesis: A is closed
then A = [#] (X | ([#] X))
.= [#] X by PRE_TOPC:def_5 ;
hence  A is closed ; ::_thesis: verum
end;
hence  ex b1 being SubSpace of X st
( b1 is strict & b1 is closed & not b1 is empty ) ; ::_thesis: verum
end;
end;

definition
let XX be non empty TopSpace;
let X be non empty closed SubSpace of XX;
let D be u.s.c._decomposition of X;
:: original: TrivExt
redefine func TrivExt D ->  u.s.c._decomposition of XX;
correctness
coherence
TrivExt D is u.s.c._decomposition of XX;
proof
let A be Subset of XX; :: according to BORSUK_1:def_10 ::_thesis: ( A in TrivExt D implies for V being a_neighborhood of A ex W being Subset of XX st
( W is open & A c= W & W c= V & ( for B being Subset of XX st B in TrivExt D & B meets W holds
B c= W ) ) )
assume A1: A in TrivExt D ; ::_thesis: for V being a_neighborhood of A ex W being Subset of XX st
( W is open & A c= W & W c= V & ( for B being Subset of XX st B in TrivExt D & B meets W holds
B c= W ) )
let V be a_neighborhood of A; ::_thesis: ex W being Subset of XX st
( W is open & A c= W & W c= V & ( for B being Subset of XX st B in TrivExt D & B meets W holds
B c= W ) )
A2: A c= Int V by CONNSP_2:def_2;
A3: Int V c= V by TOPS_1:16;
now__::_thesis:_ex_H_being_Element_of_bool_the_carrier_of_XX_st_
(_H_is_open_&_A_c=_H_&_H_c=_V_&_(_for_B_being_Subset_of_XX_st_B_in_TrivExt_D_&_B_meets_H_holds_
B_c=_H_)_)
percases ( A in D or ex x being Point of XX st
( not x in [#] X & A = {x} ) ) by A1, Th31;
supposeA4: A in D ; ::_thesis: ex H being Element of bool the carrier of XX st
( H is open & A c= H & H c= V & ( for B being Subset of XX st B in TrivExt D & B meets H holds
B c= H ) )
then reconsider C = A as Subset of X ;
reconsider E = (Int V) /\ ([#] X) as Subset of X ;
 ( E is open & C c= E ) by A2, TOPS_2:24, XBOOLE_1:19;
then  C c= Int E by TOPS_1:23;
then  E is a_neighborhood of C by CONNSP_2:def_2;
then consider W being Subset of X such that
A5: W is open and
A6: C c= W and
A7: W c= E and
A8: for B being Subset of X st B in D & B meets W holds
B c= W by A4, Def10;
consider G being Subset of XX such that
A9: G is open and
A10: W = G /\ ([#] X) by A5, TOPS_2:24;
take H = G /\ (Int V); ::_thesis: ( H is open & A c= H & H c= V & ( for B being Subset of XX st B in TrivExt D & B meets H holds
B c= H ) )
thus  H is open by A9; ::_thesis: ( A c= H & H c= V & ( for B being Subset of XX st B in TrivExt D & B meets H holds
B c= H ) )
A11: W c= G by A10, XBOOLE_1:17;
then  C c= G by A6, XBOOLE_1:1;
hence  A c= H by A2, XBOOLE_1:19; ::_thesis: ( H c= V & ( for B being Subset of XX st B in TrivExt D & B meets H holds
B c= H ) )
 H c= Int V by XBOOLE_1:17;
hence  H c= V by A3, XBOOLE_1:1; ::_thesis: for B being Subset of XX st B in TrivExt D & B meets H holds
B c= H
let B be Subset of XX; ::_thesis: ( B in TrivExt D & B meets H implies B c= H )
assume that
A12: B in TrivExt D and
A13: B meets H ; ::_thesis: B c= H
 E c= Int V by XBOOLE_1:17;
then  W c= Int V by A7, XBOOLE_1:1;
then A14: W c= H by A11, XBOOLE_1:19;
now__::_thesis:_B_c=_H
percases ( B in D or ex y being Point of XX st
( not y in [#] X & B = {y} ) ) by A12, Th31;
supposeA15: B in D ; ::_thesis: B c= H
 B meets G by A13, XBOOLE_1:74;
then  B meets W by A10, A15, XBOOLE_1:77;
then  B c= W by A8, A15;
hence  B c= H by A14, XBOOLE_1:1; ::_thesis: verum
end;
suppose ex y being Point of XX st
( not y in [#] X & B = {y} ) ; ::_thesis: B c= H
then consider y being Point of XX such that
 not y in [#] X and
A16: B = {y} ;
 y in H by A13, A16, ZFMISC_1:50;
hence  B c= H by A16, ZFMISC_1:31; ::_thesis: verum
end;
end;
end;
hence  B c= H ; ::_thesis: verum
end;
supposeA17: ex x being Point of XX st
( not x in [#] X & A = {x} ) ; ::_thesis: ex W being Element of bool the carrier of XX st
( W is open & A c= W & W c= V & ( for B being Subset of XX st B in TrivExt D & B meets W holds
B c= W ) )
 [#] X c= [#] XX by PRE_TOPC:def_4;
then reconsider C = [#] X as Subset of XX ;
take W = (Int V) \ C; ::_thesis: ( W is open & A c= W & W c= V & ( for B being Subset of XX st B in TrivExt D & B meets W holds
B c= W ) )
 C is closed by Def11;
then  (Int V) /\ (C `) is open ;
hence  W is open by SUBSET_1:13; ::_thesis: ( A c= W & W c= V & ( for B being Subset of XX st B in TrivExt D & B meets W holds
B c= W ) )
consider x being Point of XX such that
A18: not x in [#] X and
A19: A = {x} by A17;
 x in A by A19, TARSKI:def_1;
then  x in W by A2, A18, XBOOLE_0:def_5;
hence  A c= W by A19, ZFMISC_1:31; ::_thesis: ( W c= V & ( for B being Subset of XX st B in TrivExt D & B meets W holds
B c= W ) )
 W c= Int V by XBOOLE_1:36;
hence  W c= V by A3, XBOOLE_1:1; ::_thesis: for B being Subset of XX st B in TrivExt D & B meets W holds
B c= W
let B be Subset of XX; ::_thesis: ( B in TrivExt D & B meets W implies B c= W )
assume that
A20: B in TrivExt D and
A21: B meets W ; ::_thesis: B c= W
now__::_thesis:_not_B_in_D
A22: W misses C by XBOOLE_1:79;
assume  B in D ; ::_thesis: contradiction
hence  contradiction by A21, A22, XBOOLE_1:63; ::_thesis: verum
end;
then consider y being Point of XX such that
 not y in [#] X and
A23: B = {y} by A20, Th31;
 y in W by A21, A23, ZFMISC_1:50;
hence  B c= W by A23, ZFMISC_1:31; ::_thesis: verum
end;
end;
end;
hence  ex W being Subset of XX st
( W is open & A c= W & W c= V & ( for B being Subset of XX st B in TrivExt D & B meets W holds
B c= W ) ) ; ::_thesis: verum
end;
end;

definition
let X be non empty TopSpace;
let IT be u.s.c._decomposition of X;
attrIT is DECOMPOSITION-like  means :Def12: :: BORSUK_1:def 12
 for A being Subset of X st A in IT holds
A is compact ;
end;

:: deftheorem Def12 defines DECOMPOSITION-like BORSUK_1:def_12_:_
 for X being non empty TopSpace
for IT being u.s.c._decomposition of X holds
( IT is DECOMPOSITION-like iff for A being Subset of X st A in IT holds
A is compact );

registration
let X be non empty TopSpace;
cluster non empty with_non-empty_elements DECOMPOSITION-like for u.s.c._decomposition of X;
existence
 ex b1 being u.s.c._decomposition of X st b1 is DECOMPOSITION-like
proof
reconsider D = TrivDecomp X as u.s.c._decomposition of X by Th39;
take  D ; ::_thesis: D is DECOMPOSITION-like
let A be Subset of X; :: according to BORSUK_1:def_12 ::_thesis: ( A in D implies A is compact )
assume  A in D ; ::_thesis: A is compact
then  ex x being Point of X st A = {x} by Th26;
hence  A is compact ; ::_thesis: verum
end;
end;

definition
let X be non empty TopSpace;
mode DECOMPOSITION of X is DECOMPOSITION-like u.s.c._decomposition of X;
end;

definition
let XX be non empty TopSpace;
let X be non empty closed SubSpace of XX;
let D be DECOMPOSITION of X;
:: original: TrivExt
redefine func TrivExt D ->  DECOMPOSITION of XX;
correctness
coherence
TrivExt D is DECOMPOSITION of XX;
proof
 TrivExt D is DECOMPOSITION-like
proof
let A be Subset of XX; :: according to BORSUK_1:def_12 ::_thesis: ( A in TrivExt D implies A is compact )
assume  A in TrivExt D ; ::_thesis: A is compact
then consider W being Point of XX such that
A1: A = (proj (TrivExt D)) . W by EQREL_1:68;
A2: A = (Proj (TrivExt D)) . W by A1;
A3: the carrier of (space D) = D by Def7;
now__::_thesis:_A_is_compact
percases ( W in the carrier of X or not W in the carrier of X ) ;
suppose W in the carrier of X ; ::_thesis: A is compact
then reconsider W9 = W as Point of X ;
A4: A = (Proj D) . W9 by A2, Th33;
then reconsider B = A as Subset of X by A3, TARSKI:def_3;
 B is compact by A3, A4, Def12;
hence  A is compact by COMPTS_1:19; ::_thesis: verum
end;
suppose not W in the carrier of X ; ::_thesis: A is compact
then  A = {W} by A2, Th34;
hence  A is compact ; ::_thesis: verum
end;
end;
end;
hence  A is compact ; ::_thesis: verum
end;
hence  TrivExt D is DECOMPOSITION of XX ; ::_thesis: verum
end;
end;

definition
let X be non empty TopSpace;
let Y be non empty closed SubSpace of X;
let D be DECOMPOSITION of Y;
:: original: space
redefine func space D ->  strict closed SubSpace of space (TrivExt D);
correctness
coherence
space D is strict closed SubSpace of space (TrivExt D);
proof
A1: the topology of (space (TrivExt D)) =  {  A where A is Subset of (TrivExt D) : union A in the topology of X  }  by Def7;
A2: the carrier of (space (TrivExt D)) = TrivExt D by Def7;
A3: the topology of (space D) =  {  A where A is Subset of D : union A in the topology of Y  }  by Def7;
A4: the carrier of (space D) = D by Def7;
A5: ( [#] (space D) = D & [#] (space (TrivExt D)) = TrivExt D ) by Def7;
now__::_thesis:_(_[#]_(space_D)_c=_[#]_(space_(TrivExt_D))_&_(_for_P_being_Subset_of_(space_D)_holds_
(_(_P_in_the_topology_of_(space_D)_implies_ex_Q_being_Subset_of_(space_(TrivExt_D))_st_
(_Q_in_the_topology_of_(space_(TrivExt_D))_&_P_=_Q_/\_([#]_(space_D))_)_)_&_(_ex_Q_being_Subset_of_(space_(TrivExt_D))_st_
(_Q_in_the_topology_of_(space_(TrivExt_D))_&_P_=_Q_/\_([#]_(space_D))_)_implies_P_in_the_topology_of_(space_D)_)_)_)_)
thus  [#] (space D) c= [#] (space (TrivExt D)) by A5, XBOOLE_1:7; ::_thesis: for P being Subset of (space D) holds
( ( P in the topology of (space D) implies ex Q being Subset of (space (TrivExt D)) st
( Q in the topology of (space (TrivExt D)) & P = Q /\ ([#] (space D)) ) ) & ( ex Q being Subset of (space (TrivExt D)) st
( Q in the topology of (space (TrivExt D)) & P = Q /\ ([#] (space D)) ) implies P in the topology of (space D) ) )
let P be Subset of (space D); ::_thesis: ( ( P in the topology of (space D) implies ex Q being Subset of (space (TrivExt D)) st
( Q in the topology of (space (TrivExt D)) & P = Q /\ ([#] (space D)) ) ) & ( ex Q being Subset of (space (TrivExt D)) st
( Q in the topology of (space (TrivExt D)) & P = Q /\ ([#] (space D)) ) implies P in the topology of (space D) ) )
thus  ( P in the topology of (space D) implies ex Q being Subset of (space (TrivExt D)) st
( Q in the topology of (space (TrivExt D)) & P = Q /\ ([#] (space D)) ) ) ::_thesis: ( ex Q being Subset of (space (TrivExt D)) st
( Q in the topology of (space (TrivExt D)) & P = Q /\ ([#] (space D)) ) implies P in the topology of (space D) )
proof
 D c= TrivExt D by XBOOLE_1:7;
then A6: P c= TrivExt D by A4, XBOOLE_1:1;
assume  P in the topology of (space D) ; ::_thesis: ex Q being Subset of (space (TrivExt D)) st
( Q in the topology of (space (TrivExt D)) & P = Q /\ ([#] (space D)) )
then consider A being Subset of D such that
A7: P = A and
A8: union A in the topology of Y by A3;
reconsider B = union A as Subset of Y by A8;
consider C being Subset of X such that
A9: C in the topology of X and
A10: B = C /\ ([#] Y) by A8, PRE_TOPC:def_4;
  {  {x} where x is Point of X : x in C \ ([#] Y)  }  c= TrivExt D
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in  {  {x} where x is Point of X : x in C \ ([#] Y)  }  or e in TrivExt D )
assume  e in  {  {x} where x is Point of X : x in C \ ([#] Y)  }  ; ::_thesis: e in TrivExt D
then consider x being Point of X such that
A11: e = {x} and
A12: x in C \ ([#] Y) ;
 not x in the carrier of Y by A12, XBOOLE_0:def_5;
hence  e in TrivExt D by A11, Th32; ::_thesis: verum
end;
then reconsider Q = P \/  {  {x} where x is Point of X : x in C \ ([#] Y)  }  as Subset of (space (TrivExt D)) by A2, A6, XBOOLE_1:8;
take  Q ; ::_thesis: ( Q in the topology of (space (TrivExt D)) & P = Q /\ ([#] (space D)) )
now__::_thesis:_for_e_being_set_holds_
(_(_e_in_C_implies_ex_u_being_set_st_
(_e_in_u_&_u_in_Q_)_)_&_(_ex_u_being_set_st_
(_e_in_u_&_u_in_Q_)_implies_e_in_C_)_)
let e be set ; ::_thesis: ( ( e in C implies ex u being set st
( e in u & u in Q ) ) & ( ex u being set st
( e in u & u in Q ) implies e in C ) )
thus  ( e in C implies ex u being set st
( e in u & u in Q ) ) ::_thesis: ( ex u being set st
( e in u & u in Q ) implies e in C )
proof
assume A13: e in C ; ::_thesis: ex u being set st
( e in u & u in Q )
then reconsider x = e as Point of X ;
now__::_thesis:_(_(_e_in_[#]_Y_&_ex_u_being_set_st_
(_e_in_u_&_u_in_Q_)_)_or_(_not_e_in_[#]_Y_&_ex_u_being_set_st_
(_e_in_u_&_u_in_Q_)_)_)
percases ( e in [#] Y or not e in [#] Y ) ;
case e in [#] Y ; ::_thesis: ex u being set st
( e in u & u in Q )
then  e in B by A10, A13, XBOOLE_0:def_4;
then consider u being set  such that
A14: ( e in u & u in P ) by A7, TARSKI:def_4;
take u = u; ::_thesis: ( e in u & u in Q )
thus  ( e in u & u in Q ) by A14, XBOOLE_0:def_3; ::_thesis: verum
end;
caseA15: not e in [#] Y ; ::_thesis: ex u being set st
( e in u & u in Q )
take u = {e}; ::_thesis: ( e in u & u in Q )
thus  e in u by TARSKI:def_1; ::_thesis: u in Q
 x in C \ ([#] Y) by A13, A15, XBOOLE_0:def_5;
then  u in  {  {y} where y is Point of X : y in C \ ([#] Y)  }  ;
hence  u in Q by XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
hence  ex u being set st
( e in u & u in Q ) ; ::_thesis: verum
end;
given u being set  such that A16: e in u and
A17: u in Q ; ::_thesis: e in C
now__::_thesis:_e_in_C
percases ( u in P or u in  {  {x} where x is Point of X : x in C \ ([#] Y)  }  ) by A17, XBOOLE_0:def_3;
suppose u in P ; ::_thesis: e in C
then  e in B by A7, A16, TARSKI:def_4;
hence  e in C by A10, XBOOLE_0:def_4; ::_thesis: verum
end;
suppose u in  {  {x} where x is Point of X : x in C \ ([#] Y)  }  ; ::_thesis: e in C
then consider x being Point of X such that
A18: u = {x} and
A19: x in C \ ([#] Y) ;
 e = x by A16, A18, TARSKI:def_1;
hence  e in C by A19, XBOOLE_0:def_5; ::_thesis: verum
end;
end;
end;
hence  e in C ; ::_thesis: verum
end;
then  C = union Q by TARSKI:def_4;
hence  Q in the topology of (space (TrivExt D)) by A2, A1, A9; ::_thesis: P = Q /\ ([#] (space D))
 P c= Q by XBOOLE_1:7;
hence  P c= Q /\ ([#] (space D)) by XBOOLE_1:19; :: according to XBOOLE_0:def_10 ::_thesis: Q /\ ([#] (space D)) c= P
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in Q /\ ([#] (space D)) or e in P )
assume A20: e in Q /\ ([#] (space D)) ; ::_thesis: e in P
then A21: e in [#] (space D) ;
A22: now__::_thesis:_not_e_in__{__{x}_where_x_is_Point_of_X_:_x_in_C_\_([#]_Y)__}_
assume  e in  {  {x} where x is Point of X : x in C \ ([#] Y)  }  ; ::_thesis: contradiction
then consider x being Point of X such that
A23: e = {x} and
A24: x in C \ ([#] Y) ;
A25: not x in the carrier of Y by A24, XBOOLE_0:def_5;
then  not (Proj (TrivExt D)) . x in the carrier of (space D) by Th36;
hence  contradiction by A21, A23, A25, Th34; ::_thesis: verum
end;
 e in Q by A20, XBOOLE_0:def_4;
hence  e in P by A22, XBOOLE_0:def_3; ::_thesis: verum
end;
given Q being Subset of (space (TrivExt D)) such that A26: Q in the topology of (space (TrivExt D)) and
A27: P = Q /\ ([#] (space D)) ; ::_thesis: P in the topology of (space D)
A28: union P is Subset of Y by A4, EQREL_1:61;
now__::_thesis:_for_e_being_set_holds_
(_(_e_in_(union_Q)_/\_([#]_Y)_implies_ex_u_being_set_st_
(_e_in_u_&_u_in_P_)_)_&_(_ex_u_being_set_st_
(_e_in_u_&_u_in_P_)_implies_e_in_(union_Q)_/\_([#]_Y)_)_)
let e be set ; ::_thesis: ( ( e in (union Q) /\ ([#] Y) implies ex u being set st
( e in u & u in P ) ) & ( ex u being set st
( e in u & u in P ) implies e in (union Q) /\ ([#] Y) ) )
thus  ( e in (union Q) /\ ([#] Y) implies ex u being set st
( e in u & u in P ) ) ::_thesis: ( ex u being set st
( e in u & u in P ) implies e in (union Q) /\ ([#] Y) )
proof
assume A29: e in (union Q) /\ ([#] Y) ; ::_thesis: ex u being set st
( e in u & u in P )
then A30: (Proj (TrivExt D)) . e in the carrier of (space D) by Th37;
 e in union Q by A29, XBOOLE_0:def_4;
then consider u being set  such that
A31: e in u and
A32: u in Q by TARSKI:def_4;
take  u ; ::_thesis: ( e in u & u in P )
thus  e in u by A31; ::_thesis: u in P
 u is Element of TrivExt D by A32, Def7;
then  u = (Proj (TrivExt D)) . e by A31, EQREL_1:65;
hence  u in P by A27, A32, A30, XBOOLE_0:def_4; ::_thesis: verum
end;
given u being set  such that A33: e in u and
A34: u in P ; ::_thesis: e in (union Q) /\ ([#] Y)
 u in Q by A27, A34, XBOOLE_0:def_4;
then A35: e in union Q by A33, TARSKI:def_4;
 e in union P by A33, A34, TARSKI:def_4;
hence  e in (union Q) /\ ([#] Y) by A28, A35, XBOOLE_0:def_4; ::_thesis: verum
end;
then A36: union P = (union Q) /\ ([#] Y) by TARSKI:def_4;
 ex A being Subset of (TrivExt D) st
( Q = A & union A in the topology of X ) by A1, A26;
then  union P in the topology of Y by A36, PRE_TOPC:def_4;
hence  P in the topology of (space D) by A4, A3; ::_thesis: verum
end;
then reconsider T = space D as SubSpace of space (TrivExt D) by PRE_TOPC:def_4;
 T is closed
proof
let A be Subset of (space (TrivExt D)); :: according to BORSUK_1:def_11 ::_thesis: ( A = the carrier of T implies A is closed )
assume A37: A = the carrier of T ; ::_thesis: A is closed
reconsider C = A ` as Subset of (TrivExt D) by Def7;
reconsider B = union A as Subset of X by A2, EQREL_1:61;
 B = the carrier of Y by A4, A37, EQREL_1:def_4;
then  B is closed by Def11;
then A38: B ` in the topology of X by PRE_TOPC:def_2;
 union C = B ` by A2, EQREL_1:63;
then  A ` in the topology of (space (TrivExt D)) by A38, Th27;
then  A ` is open by PRE_TOPC:def_2;
hence  A is closed by TOPS_1:3; ::_thesis: verum
end;
hence  space D is strict closed SubSpace of space (TrivExt D) ; ::_thesis: verum
end;
end;

begin

Lm3:  TopSpaceMetr RealSpace = TopStruct(# the carrier of RealSpace,(Family_open_set RealSpace) #)
by PCOMPS_1:def_5;

definition
func I[01]  ->  TopStruct  means :Def13: :: BORSUK_1:def 13
 for P being Subset of (TopSpaceMetr RealSpace) st P = [.0,1.] holds
it = (TopSpaceMetr RealSpace) | P;
existence
 ex b1 being TopStruct st
for P being Subset of (TopSpaceMetr RealSpace) st P = [.0,1.] holds
b1 = (TopSpaceMetr RealSpace) | P
proof
reconsider P = [.0,1.] as non empty Subset of (TopSpaceMetr RealSpace) by Lm3, METRIC_1:def_13, XXREAL_1:1;
take  (TopSpaceMetr RealSpace) | P ; ::_thesis: for P being Subset of (TopSpaceMetr RealSpace) st P = [.0,1.] holds
(TopSpaceMetr RealSpace) | P = (TopSpaceMetr RealSpace) | P
thus  for P being Subset of (TopSpaceMetr RealSpace) st P = [.0,1.] holds
(TopSpaceMetr RealSpace) | P = (TopSpaceMetr RealSpace) | P ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being TopStruct st ( for P being Subset of (TopSpaceMetr RealSpace) st P = [.0,1.] holds
b1 = (TopSpaceMetr RealSpace) | P ) & ( for P being Subset of (TopSpaceMetr RealSpace) st P = [.0,1.] holds
b2 = (TopSpaceMetr RealSpace) | P ) holds
b1 = b2
proof
reconsider P = [.0,1.] as Subset of (TopSpaceMetr RealSpace) by Lm3, METRIC_1:def_13;
let I1, I2 be TopStruct ; ::_thesis: ( ( for P being Subset of (TopSpaceMetr RealSpace) st P = [.0,1.] holds
I1 = (TopSpaceMetr RealSpace) | P ) & ( for P being Subset of (TopSpaceMetr RealSpace) st P = [.0,1.] holds
I2 = (TopSpaceMetr RealSpace) | P ) implies I1 = I2 )
assume that
A1: for P being Subset of (TopSpaceMetr RealSpace) st P = [.0,1.] holds
I1 = (TopSpaceMetr RealSpace) | P and
A2: for P being Subset of (TopSpaceMetr RealSpace) st P = [.0,1.] holds
I2 = (TopSpaceMetr RealSpace) | P ; ::_thesis: I1 = I2
 I1 = (TopSpaceMetr RealSpace) | P by A1;
hence  I1 = I2 by A2; ::_thesis: verum
end;
end;

:: deftheorem Def13 defines I[01] BORSUK_1:def_13_:_
 for b1 being TopStruct holds
( b1 = I[01] iff for P being Subset of (TopSpaceMetr RealSpace) st P = [.0,1.] holds
b1 = (TopSpaceMetr RealSpace) | P );

registration
cluster I[01]  ->  non empty strict TopSpace-like ;
coherence
 ( I[01] is strict & not I[01] is empty & I[01] is TopSpace-like )
proof
reconsider P = [.0,1.] as non empty Subset of (TopSpaceMetr RealSpace) by Lm3, METRIC_1:def_13, XXREAL_1:1;
 I[01] = (TopSpaceMetr RealSpace) | P by Def13;
hence  ( I[01] is strict & not I[01] is empty & I[01] is TopSpace-like ) ; ::_thesis: verum
end;
end;

theorem Th40: :: BORSUK_1:40
the carrier of I[01] = [.0,1.]
proof
reconsider P = [.0,1.] as Subset of (TopSpaceMetr RealSpace) by Lm3, METRIC_1:def_13;
A1: I[01] = (TopSpaceMetr RealSpace) | P by Def13;
thus  the carrier of I[01] = [#] I[01]
.= [.0,1.] by A1, PRE_TOPC:def_5 ; ::_thesis: verum
end;

definition
func 0[01]  ->  Point of I[01] equals :: BORSUK_1:def 14
 0 ;
coherence
 0 is Point of I[01] by Th40, XXREAL_1:1;
func 1[01]  ->  Point of I[01] equals :: BORSUK_1:def 15
1;
coherence
 1 is Point of I[01] by Th40, XXREAL_1:1;
end;

:: deftheorem  defines 0[01] BORSUK_1:def_14_:_
 0[01] = 0 ;

:: deftheorem  defines 1[01] BORSUK_1:def_15_:_
 1[01] = 1;

definition
let A be non empty TopSpace;
let B be non empty SubSpace of A;
let F be Function of A,B;
attrF is being_a_retraction  means :Def16: :: BORSUK_1:def 16
 for W being Point of A st W in the carrier of B holds
F . W = W;
end;

:: deftheorem Def16 defines being_a_retraction BORSUK_1:def_16_:_
 for A being non empty TopSpace
for B being non empty SubSpace of A
for F being Function of A,B holds
( F is being_a_retraction iff for W being Point of A st W in the carrier of B holds
F . W = W );

definition
let X be non empty TopSpace;
let Y be non empty SubSpace of X;
predY is_a_retract_of X means :: BORSUK_1:def 17
 ex F being continuous Function of X,Y st F is being_a_retraction ;
predY is_an_SDR_of X means :: BORSUK_1:def 18
 ex H being continuous Function of [:X,I[01]:],X st
for A being Point of X holds
( H . [A,0[01]] = A & H . [A,1[01]] in the carrier of Y & ( A in the carrier of Y implies for T being Point of I[01] holds H . [A,T] = A ) );
end;

:: deftheorem  defines is_a_retract_of BORSUK_1:def_17_:_
 for X being non empty TopSpace
for Y being non empty SubSpace of X holds
( Y is_a_retract_of X iff ex F being continuous Function of X,Y st F is being_a_retraction );

:: deftheorem  defines is_an_SDR_of BORSUK_1:def_18_:_
 for X being non empty TopSpace
for Y being non empty SubSpace of X holds
( Y is_an_SDR_of X iff ex H being continuous Function of [:X,I[01]:],X st
for A being Point of X holds
( H . [A,0[01]] = A & H . [A,1[01]] in the carrier of Y & ( A in the carrier of Y implies for T being Point of I[01] holds H . [A,T] = A ) ) );

theorem :: BORSUK_1:41
for XX being non empty TopSpace
for X being non empty closed SubSpace of XX
for D being DECOMPOSITION of X st X is_a_retract_of XX holds
space D is_a_retract_of space (TrivExt D)
proof
let XX be non empty TopSpace; ::_thesis: for X being non empty closed SubSpace of XX
for D being DECOMPOSITION of X st X is_a_retract_of XX holds
space D is_a_retract_of space (TrivExt D)
let X be non empty closed SubSpace of XX; ::_thesis: for D being DECOMPOSITION of X st X is_a_retract_of XX holds
space D is_a_retract_of space (TrivExt D)
let D be DECOMPOSITION of X; ::_thesis: ( X is_a_retract_of XX implies space D is_a_retract_of space (TrivExt D) )
thus  ( X is_a_retract_of XX implies space D is_a_retract_of space (TrivExt D) ) ::_thesis: verum
proof
given R being continuous Function of XX,X such that A1: R is being_a_retraction ; :: according to BORSUK_1:def_17 ::_thesis: space D is_a_retract_of space (TrivExt D)
now__::_thesis:_for_xx,_xx9_being_Point_of_XX_holds_
(_not_(Proj_(TrivExt_D))_._xx_=_(Proj_(TrivExt_D))_._xx9_or_not_((Proj_D)_*_R)_._xx_<>_((Proj_D)_*_R)_._xx9_)
given xx, xx9 being Point of XX such that A2: ( (Proj (TrivExt D)) . xx = (Proj (TrivExt D)) . xx9 & ((Proj D) * R) . xx <> ((Proj D) * R) . xx9 ) ; ::_thesis: contradiction
 xx in the carrier of X by A2, Th35;
then  R . xx = xx by A1, Def16;
then A3: (Proj D) . xx = ((Proj D) * R) . xx by FUNCT_2:15;
 xx9 in the carrier of X by A2, Th35;
then A4: R . xx9 = xx9 by A1, Def16;
 ( (Proj (TrivExt D)) . xx = (Proj D) . xx & (Proj (TrivExt D)) . xx9 = (Proj D) . xx9 ) by A2, Th33, Th35;
hence  contradiction by A2, A4, A3, FUNCT_2:15; ::_thesis: verum
end;
then consider F being Function of the carrier of (space (TrivExt D)), the carrier of (space D) such that
A5: F * (Proj (TrivExt D)) = (Proj D) * R by EQREL_1:56;
reconsider F = F as Function of (space (TrivExt D)),(space D) ;
 F is continuous
proof
let W be Point of (space (TrivExt D)); :: according to BORSUK_1:def_1 ::_thesis: for G being a_neighborhood of F . W ex H being a_neighborhood of W st F .: H c= G
let G be a_neighborhood of F . W; ::_thesis: ex H being a_neighborhood of W st F .: H c= G
reconsider GG = ((Proj D) * R) " G as a_neighborhood of (Proj (TrivExt D)) " {W} by A5, Th4, EQREL_1:57;
reconsider V9 = (Proj (TrivExt D)) .: GG as a_neighborhood of W by Th38;
take V = V9; ::_thesis: F .: V c= G
 F .: V = ((Proj D) * R) .: GG by A5, RELAT_1:126;
hence  F .: V c= G by FUNCT_1:75; ::_thesis: verum
end;
then reconsider F9 = F as continuous Function of (space (TrivExt D)),(space D) ;
take  F9 ; :: according to BORSUK_1:def_17 ::_thesis: F9 is being_a_retraction
let W be Point of (space (TrivExt D)); :: according to BORSUK_1:def_16 ::_thesis: ( W in the carrier of (space D) implies F9 . W = W )
consider W9 being Point of XX such that
A6: (Proj (TrivExt D)) . W9 = W by Th29;
assume A7: W in the carrier of (space D) ; ::_thesis: F9 . W = W
then  W9 in the carrier of X by A6, Th36;
then A8: W9 = R . W9 by A1, Def16;
A9: F9 . W = (F * (Proj (TrivExt D))) . W9 by A6, FUNCT_2:15;
 (Proj D) . W9 = (Proj (TrivExt D)) . W9 by A6, A7, Th33, Th36;
hence  F9 . W = W by A5, A6, A8, A9, FUNCT_2:15; ::_thesis: verum
end;
end;

theorem :: BORSUK_1:42
for XX being non empty TopSpace
for X being non empty closed SubSpace of XX
for D being DECOMPOSITION of X st X is_an_SDR_of XX holds
space D is_an_SDR_of space (TrivExt D)
proof
let XX be non empty TopSpace; ::_thesis: for X being non empty closed SubSpace of XX
for D being DECOMPOSITION of X st X is_an_SDR_of XX holds
space D is_an_SDR_of space (TrivExt D)
let X be non empty closed SubSpace of XX; ::_thesis: for D being DECOMPOSITION of X st X is_an_SDR_of XX holds
space D is_an_SDR_of space (TrivExt D)
let D be DECOMPOSITION of X; ::_thesis: ( X is_an_SDR_of XX implies space D is_an_SDR_of space (TrivExt D) )
given CH1 being continuous Function of [:XX,I[01]:],XX such that A1: for A being Point of XX holds
( CH1 . [A,0[01]] = A & CH1 . [A,1[01]] in the carrier of X & ( A in the carrier of X implies for T being Point of I[01] holds CH1 . [A,T] = A ) ) ; :: according to BORSUK_1:def_18 ::_thesis: space D is_an_SDR_of space (TrivExt D)
 the carrier of [:XX,I[01]:] = [: the carrier of XX, the carrier of I[01]:] by Def2;
then reconsider II = [:(Proj (TrivExt D)),(id the carrier of I[01]):] as Function of the carrier of [:XX,I[01]:], the carrier of [:(space (TrivExt D)),I[01]:] by Def2;
now__::_thesis:_for_xx,_xx9_being_Point_of_[:XX,I[01]:]_holds_
(_not_II_._xx_=_II_._xx9_or_not_((Proj_(TrivExt_D))_*_CH1)_._xx_<>_((Proj_(TrivExt_D))_*_CH1)_._xx9_)
given xx, xx9 being Point of [:XX,I[01]:] such that A2: II . xx = II . xx9 and
A3: ((Proj (TrivExt D)) * CH1) . xx <> ((Proj (TrivExt D)) * CH1) . xx9 ; ::_thesis: contradiction
A4: ( ((Proj (TrivExt D)) * CH1) . xx = (Proj (TrivExt D)) . (CH1 . xx) & ((Proj (TrivExt D)) * CH1) . xx9 = (Proj (TrivExt D)) . (CH1 . xx9) ) by FUNCT_2:15;
consider x being Point of XX, t being Point of I[01] such that
A5: xx = [x,t] by Th10;
consider x9 being Point of XX, t9 being Point of I[01] such that
A6: xx9 = [x9,t9] by Th10;
A7: ( II . (x,t) = [((Proj (TrivExt D)) . x),t] & II . (x9,t9) = [((Proj (TrivExt D)) . x9),t9] ) by EQREL_1:58;
then  ( t = t9 & (Proj (TrivExt D)) . x = (Proj (TrivExt D)) . x9 ) by A2, A5, A6, XTUPLE_0:1;
then  ( CH1 . xx = x & CH1 . xx9 = x9 ) by A1, A3, A5, A6, Th35;
hence  contradiction by A2, A3, A5, A6, A7, A4, XTUPLE_0:1; ::_thesis: verum
end;
then consider THETA being Function of the carrier of [:(space (TrivExt D)),I[01]:], the carrier of (space (TrivExt D)) such that
A8: (Proj (TrivExt D)) * CH1 = THETA * II by EQREL_1:56;
reconsider THETA = THETA as Function of [:(space (TrivExt D)),I[01]:],(space (TrivExt D)) ;
 THETA is continuous
proof
let WT be Point of [:(space (TrivExt D)),I[01]:]; :: according to BORSUK_1:def_1 ::_thesis: for G being a_neighborhood of THETA . WT ex H being a_neighborhood of WT st THETA .: H c= G
reconsider xt9 = WT as Element of [: the carrier of (space (TrivExt D)), the carrier of I[01]:] by Def2;
let G be a_neighborhood of THETA . WT; ::_thesis: ex H being a_neighborhood of WT st THETA .: H c= G
reconsider FF = (Proj (TrivExt D)) * CH1 as continuous Function of [:XX,I[01]:],(space (TrivExt D)) ;
consider W being Point of (space (TrivExt D)), T being Point of I[01] such that
A9: WT = [W,T] by Th10;
 II " {xt9} = [:((Proj (TrivExt D)) " {W}),{T}:] by A9, EQREL_1:60;
then reconsider GG = FF " G as a_neighborhood of [:((Proj (TrivExt D)) " {W}),{T}:] by A8, Th4, EQREL_1:57;
 W in the carrier of (space (TrivExt D)) ;
then A10: W in TrivExt D by Def7;
then  (Proj (TrivExt D)) " {W} = W by EQREL_1:66;
then  (Proj (TrivExt D)) " {W} is compact by A10, Def12;
then consider U being a_neighborhood of (Proj (TrivExt D)) " {W}, V being a_neighborhood of T such that
A11: [:U,V:] c= GG by Th25;
reconsider H9 = (Proj (TrivExt D)) .: U as a_neighborhood of W by Th38;
reconsider H99 = [:H9,V:] as a_neighborhood of WT by A9;
take H = H99; ::_thesis: THETA .: H c= G
 II .: [:U,V:] = [:((Proj (TrivExt D)) .: U),V:] by EQREL_1:59;
then A12: ( ((Proj (TrivExt D)) * CH1) .: GG c= G & THETA .: H = ((Proj (TrivExt D)) * CH1) .: [:U,V:] ) by A8, FUNCT_1:75, RELAT_1:126;
 ((Proj (TrivExt D)) * CH1) .: [:U,V:] c= ((Proj (TrivExt D)) * CH1) .: GG by A11, RELAT_1:123;
hence  THETA .: H c= G by A12, XBOOLE_1:1; ::_thesis: verum
end;
then reconsider THETA9 = THETA as continuous Function of [:(space (TrivExt D)),I[01]:],(space (TrivExt D)) ;
take THETA99 = THETA9; :: according to BORSUK_1:def_18 ::_thesis: for A being Point of (space (TrivExt D)) holds
( THETA99 . [A,0[01]] = A & THETA99 . [A,1[01]] in the carrier of (space D) & ( A in the carrier of (space D) implies for T being Point of I[01] holds THETA99 . [A,T] = A ) )
let W be Point of (space (TrivExt D)); ::_thesis: ( THETA99 . [W,0[01]] = W & THETA99 . [W,1[01]] in the carrier of (space D) & ( W in the carrier of (space D) implies for T being Point of I[01] holds THETA99 . [W,T] = W ) )
consider W9 being Point of XX such that
A13: (Proj (TrivExt D)) . W9 = W by Th29;
 II . (W9,0[01]) = [W,0[01]] by A13, EQREL_1:58;
then A14: (THETA9 * II) . [W9,0[01]] = THETA9 . [W,0[01]] by FUNCT_2:15;
 CH1 . (W9,0[01]) = W9 by A1;
hence  THETA99 . [W,0[01]] = W by A8, A13, A14, FUNCT_2:15; ::_thesis: ( THETA99 . [W,1[01]] in the carrier of (space D) & ( W in the carrier of (space D) implies for T being Point of I[01] holds THETA99 . [W,T] = W ) )
A15: CH1 . [W9,1[01]] in the carrier of X by A1;
 II . (W9,1[01]) = [W,1[01]] by A13, EQREL_1:58;
then A16: (THETA9 * II) . [W9,1[01]] = THETA9 . [W,1[01]] by FUNCT_2:15;
 (THETA9 * II) . [W9,1[01]] = (Proj (TrivExt D)) . (CH1 . [W9,1[01]]) by A8, FUNCT_2:15;
hence  THETA99 . [W,1[01]] in the carrier of (space D) by A16, A15, Th37; ::_thesis: ( W in the carrier of (space D) implies for T being Point of I[01] holds THETA99 . [W,T] = W )
assume A17: W in the carrier of (space D) ; ::_thesis: for T being Point of I[01] holds THETA99 . [W,T] = W
let T be Point of I[01]; ::_thesis: THETA99 . [W,T] = W
 II . (W9,T) = [W,T] by A13, EQREL_1:58;
then A18: (THETA9 * II) . [W9,T] = THETA9 . [W,T] by FUNCT_2:15;
 CH1 . (W9,T) = W9 by A1, A13, A17, Th36;
hence  THETA99 . [W,T] = W by A8, A13, A18, FUNCT_2:15; ::_thesis: verum
end;

theorem :: BORSUK_1:43
for r being real number holds
( ( 0 <= r & r <= 1 ) iff r in the carrier of I[01] )
proof
let r be real number ; ::_thesis: ( ( 0 <= r & r <= 1 ) iff r in the carrier of I[01] )
A1: [.0,1.] =  {  r1 where r1 is Real : ( 0 <= r1 & r1 <= 1 )  }  by RCOMP_1:def_1;
 r is Real by XREAL_0:def_1;
hence  ( 0 <= r & r <= 1 implies r in the carrier of I[01] ) by A1, Th40; ::_thesis: ( r in the carrier of I[01] implies ( 0 <= r & r <= 1 ) )
assume  r in the carrier of I[01] ; ::_thesis: ( 0 <= r & r <= 1 )
then  ex r2 being Real st
( r2 = r & 0 <= r2 & r2 <= 1 ) by A1, Th40;
hence  ( 0 <= r & r <= 1 ) ; ::_thesis: verum
end;