:: BORSUK_3 semantic presentation

begin

theorem :: BORSUK_3:1
for S, T being TopSpace holds [#] [:S,T:] = [:([#] S),([#] T):] by BORSUK_1:def_2;

theorem Th2: :: BORSUK_3:2
for X, Y being non empty TopSpace
for x being Point of X holds Y --> x is continuous Function of Y,(X | {x})
proof
let X, Y be non empty TopSpace; ::_thesis: for x being Point of X holds Y --> x is continuous Function of Y,(X | {x})
let x be Point of X; ::_thesis: Y --> x is continuous Function of Y,(X | {x})
set Z = {x};
set f = Y --> x;
 ( x in {x} & the carrier of (X | {x}) = {x} ) by PRE_TOPC:8, TARSKI:def_1;
then reconsider g = Y --> x as Function of Y,(X | {x}) by FUNCOP_1:45;
 g is continuous by TOPMETR:6;
hence  Y --> x is continuous Function of Y,(X | {x}) ; ::_thesis: verum
end;

registration
let T be TopStruct ;
cluster id T ->  being_homeomorphism ;
coherence
 id T is being_homeomorphism by TOPGRP_1:20;
end;

Lm1:  for S being TopStruct holds S,S are_homeomorphic
proof
let S be TopStruct ; ::_thesis: S,S are_homeomorphic
take  id S ; :: according to T_0TOPSP:def_1 ::_thesis: id S is being_homeomorphism
thus  id S is being_homeomorphism ; ::_thesis: verum
end;

Lm2:  for S, T being non empty TopStruct st S,T are_homeomorphic holds
T,S are_homeomorphic
proof
let S, T be non empty TopStruct ; ::_thesis: ( S,T are_homeomorphic implies T,S are_homeomorphic )
assume  S,T are_homeomorphic ; ::_thesis: T,S are_homeomorphic
then consider f being Function of S,T such that
A1: f is being_homeomorphism by T_0TOPSP:def_1;
 f " is being_homeomorphism by A1, TOPS_2:56;
hence  T,S are_homeomorphic by T_0TOPSP:def_1; ::_thesis: verum
end;

definition
let S, T be TopStruct ;
:: original: are_homeomorphic
redefine predS,T are_homeomorphic ;
reflexivity
 for S being TopStruct holds R36(b1,b1) by Lm1;
end;

definition
let S, T be non empty TopStruct ;
:: original: are_homeomorphic
redefine predS,T are_homeomorphic ;
reflexivity
 for S being non empty TopStruct holds R36(b1,b1) by Lm1;
symmetry
 for S, T being non empty TopStruct st R36(b1,b2) holds
R36(b2,b1) by Lm2;
end;

theorem :: BORSUK_3:3
for S, T, V being non empty TopSpace st S,T are_homeomorphic & T,V are_homeomorphic holds
S,V are_homeomorphic
proof
let S, T, V be non empty TopSpace; ::_thesis: ( S,T are_homeomorphic & T,V are_homeomorphic implies S,V are_homeomorphic )
assume that
A1: S,T are_homeomorphic and
A2: T,V are_homeomorphic ; ::_thesis: S,V are_homeomorphic
consider f being Function of S,T such that
A3: f is being_homeomorphism by A1, T_0TOPSP:def_1;
consider g being Function of T,V such that
A4: g is being_homeomorphism by A2, T_0TOPSP:def_1;
 g * f is being_homeomorphism by A3, A4, TOPS_2:57;
hence  S,V are_homeomorphic by T_0TOPSP:def_1; ::_thesis: verum
end;

begin

registration
let T be TopStruct ;
let P be empty Subset of T;
clusterT | P ->  empty ;
coherence
 T | P is empty ;
end;

registration
cluster empty TopSpace-like  ->  compact for TopStruct ;
coherence
 for b1 being TopSpace st b1 is empty holds
b1 is compact ;
end;

theorem Th4: :: BORSUK_3:4
for X, Y being non empty TopSpace
for x being Point of X
for f being Function of [:Y,(X | {x}):],Y st f = pr1 ( the carrier of Y,{x}) holds
f is one-to-one
proof
let X, Y be non empty TopSpace; ::_thesis: for x being Point of X
for f being Function of [:Y,(X | {x}):],Y st f = pr1 ( the carrier of Y,{x}) holds
f is one-to-one
let x be Point of X; ::_thesis: for f being Function of [:Y,(X | {x}):],Y st f = pr1 ( the carrier of Y,{x}) holds
f is one-to-one
let f be Function of [:Y,(X | {x}):],Y; ::_thesis: ( f = pr1 ( the carrier of Y,{x}) implies f is one-to-one )
set Z = {x};
assume A1: f = pr1 ( the carrier of Y,{x}) ; ::_thesis: f is one-to-one
let z, y be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not z in dom f or not y in dom f or not f . z = f . y or z = y )
assume that
A2: z in dom f and
A3: y in dom f and
A4: f . z = f . y ; ::_thesis: z = y
A5: dom f = [: the carrier of Y,{x}:] by A1, FUNCT_3:def_4;
then consider x1, x2 being set  such that
A6: x1 in the carrier of Y and
A7: x2 in {x} and
A8: z = [x1,x2] by A2, ZFMISC_1:def_2;
consider y1, y2 being set  such that
A9: y1 in the carrier of Y and
A10: y2 in {x} and
A11: y = [y1,y2] by A5, A3, ZFMISC_1:def_2;
A12: x2 = x by A7, TARSKI:def_1
.= y2 by A10, TARSKI:def_1 ;
x1 = f . (x1,x2) by A1, A6, A7, FUNCT_3:def_4
.= f . (y1,y2) by A4, A8, A11
.= y1 by A1, A9, A10, FUNCT_3:def_4 ;
hence  z = y by A8, A11, A12; ::_thesis: verum
end;

theorem Th5: :: BORSUK_3:5
for X, Y being non empty TopSpace
for x being Point of X
for f being Function of [:(X | {x}),Y:],Y st f = pr2 ({x}, the carrier of Y) holds
f is one-to-one
proof
let X, Y be non empty TopSpace; ::_thesis: for x being Point of X
for f being Function of [:(X | {x}),Y:],Y st f = pr2 ({x}, the carrier of Y) holds
f is one-to-one
let x be Point of X; ::_thesis: for f being Function of [:(X | {x}),Y:],Y st f = pr2 ({x}, the carrier of Y) holds
f is one-to-one
let f be Function of [:(X | {x}),Y:],Y; ::_thesis: ( f = pr2 ({x}, the carrier of Y) implies f is one-to-one )
set Z = {x};
assume A1: f = pr2 ({x}, the carrier of Y) ; ::_thesis: f is one-to-one
let z, y be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not z in dom f or not y in dom f or not f . z = f . y or z = y )
assume that
A2: z in dom f and
A3: y in dom f and
A4: f . z = f . y ; ::_thesis: z = y
A5: dom f = [:{x}, the carrier of Y:] by A1, FUNCT_3:def_5;
then consider x1, x2 being set  such that
A6: x1 in {x} and
A7: x2 in the carrier of Y and
A8: z = [x1,x2] by A2, ZFMISC_1:def_2;
consider y1, y2 being set  such that
A9: y1 in {x} and
A10: y2 in the carrier of Y and
A11: y = [y1,y2] by A5, A3, ZFMISC_1:def_2;
A12: x1 = x by A6, TARSKI:def_1
.= y1 by A9, TARSKI:def_1 ;
x2 = f . (x1,x2) by A1, A6, A7, FUNCT_3:def_5
.= f . (y1,y2) by A4, A8, A11
.= y2 by A1, A9, A10, FUNCT_3:def_5 ;
hence  z = y by A8, A11, A12; ::_thesis: verum
end;

theorem Th6: :: BORSUK_3:6
for X, Y being non empty TopSpace
for x being Point of X
for f being Function of [:Y,(X | {x}):],Y st f = pr1 ( the carrier of Y,{x}) holds
f " = <:(id Y),(Y --> x):>
proof
let X, Y be non empty TopSpace; ::_thesis: for x being Point of X
for f being Function of [:Y,(X | {x}):],Y st f = pr1 ( the carrier of Y,{x}) holds
f " = <:(id Y),(Y --> x):>
let x be Point of X; ::_thesis: for f being Function of [:Y,(X | {x}):],Y st f = pr1 ( the carrier of Y,{x}) holds
f " = <:(id Y),(Y --> x):>
let f be Function of [:Y,(X | {x}):],Y; ::_thesis: ( f = pr1 ( the carrier of Y,{x}) implies f " = <:(id Y),(Y --> x):> )
set Z = {x};
set idZ = id Y;
A1: rng (id Y) c= the carrier of Y ;
assume A2: f = pr1 ( the carrier of Y,{x}) ; ::_thesis: f " = <:(id Y),(Y --> x):>
then A3: rng f = the carrier of Y by FUNCT_3:44;
reconsider Z = {x} as non empty Subset of X ;
reconsider idY = Y --> x as continuous Function of Y,(X | Z) by Th2;
reconsider KA = <:(id Y),idY:> as continuous Function of Y,[:Y,(X | Z):] by YELLOW12:41;
A4: [: the carrier of Y,Z:] c= rng KA
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in [: the carrier of Y,Z:] or y in rng KA )
assume  y in [: the carrier of Y,Z:] ; ::_thesis: y in rng KA
then consider y1, y2 being set  such that
A5: y1 in the carrier of Y and
A6: ( y2 in {x} & y = [y1,y2] ) by ZFMISC_1:def_2;
A7: y = [y1,x] by A6, TARSKI:def_1;
A8: idY . y1 = ( the carrier of Y --> x) . y1
.= x by A5, FUNCOP_1:7 ;
A9: y1 in dom KA by A5, FUNCT_2:def_1;
then KA . y1 = [((id Y) . y1),(idY . y1)] by FUNCT_3:def_7
.= [y1,x] by A5, A8, FUNCT_1:18 ;
hence  y in rng KA by A7, A9, FUNCT_1:def_3; ::_thesis: verum
end;
 rng idY c= the carrier of (X | Z) ;
then A10: rng idY c= Z by PRE_TOPC:8;
then  ( rng KA c= [:(rng (id Y)),(rng idY):] & [:(rng (id Y)),(rng idY):] c= [: the carrier of Y,Z:] ) by FUNCT_3:51, ZFMISC_1:96;
then  rng KA c= [: the carrier of Y,Z:] by XBOOLE_1:1;
then A11: rng KA = [: the carrier of Y,Z:] by A4, XBOOLE_0:def_10
.= dom f by A2, FUNCT_3:def_4 ;
A12: f is one-to-one by A2, Th4;
A13: f is onto by A3, FUNCT_2:def_3;
dom idY = the carrier of Y by FUNCT_2:def_1
.= dom (id Y) by FUNCT_2:def_1 ;
then  f * KA = id (rng f) by A2, A3, A10, A1, FUNCT_3:52;
then  KA = f " by A12, A11, FUNCT_1:42;
hence  f " = <:(id Y),(Y --> x):> by A12, A13, TOPS_2:def_4; ::_thesis: verum
end;

theorem Th7: :: BORSUK_3:7
for X, Y being non empty TopSpace
for x being Point of X
for f being Function of [:(X | {x}),Y:],Y st f = pr2 ({x}, the carrier of Y) holds
f " = <:(Y --> x),(id Y):>
proof
let X, Y be non empty TopSpace; ::_thesis: for x being Point of X
for f being Function of [:(X | {x}),Y:],Y st f = pr2 ({x}, the carrier of Y) holds
f " = <:(Y --> x),(id Y):>
let x be Point of X; ::_thesis: for f being Function of [:(X | {x}),Y:],Y st f = pr2 ({x}, the carrier of Y) holds
f " = <:(Y --> x),(id Y):>
let f be Function of [:(X | {x}),Y:],Y; ::_thesis: ( f = pr2 ({x}, the carrier of Y) implies f " = <:(Y --> x),(id Y):> )
set Z = {x};
set idY = id Y;
A1: rng (id Y) c= the carrier of Y ;
assume A2: f = pr2 ({x}, the carrier of Y) ; ::_thesis: f " = <:(Y --> x),(id Y):>
then A3: rng f = the carrier of Y by FUNCT_3:46;
reconsider Z = {x} as non empty Subset of X ;
reconsider idZ = Y --> x as continuous Function of Y,(X | Z) by Th2;
reconsider KA = <:idZ,(id Y):> as continuous Function of Y,[:(X | Z),Y:] by YELLOW12:41;
A4: [:{x}, the carrier of Y:] c= rng KA
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in [:{x}, the carrier of Y:] or y in rng KA )
assume  y in [:{x}, the carrier of Y:] ; ::_thesis: y in rng KA
then consider y1, y2 being set  such that
A5: y1 in {x} and
A6: y2 in the carrier of Y and
A7: y = [y1,y2] by ZFMISC_1:def_2;
A8: y = [x,y2] by A5, A7, TARSKI:def_1;
A9: idZ . y2 = ( the carrier of Y --> x) . y2
.= x by A6, FUNCOP_1:7 ;
A10: y2 in dom KA by A6, FUNCT_2:def_1;
then KA . y2 = [(idZ . y2),((id Y) . y2)] by FUNCT_3:def_7
.= [x,y2] by A6, A9, FUNCT_1:18 ;
hence  y in rng KA by A8, A10, FUNCT_1:def_3; ::_thesis: verum
end;
 rng idZ c= the carrier of (X | Z) ;
then A11: rng idZ c= Z by PRE_TOPC:8;
then  ( rng KA c= [:(rng idZ),(rng (id Y)):] & [:(rng idZ),(rng (id Y)):] c= [:{x}, the carrier of Y:] ) by FUNCT_3:51, ZFMISC_1:96;
then  rng KA c= [:{x}, the carrier of Y:] by XBOOLE_1:1;
then A12: rng KA = [:Z, the carrier of Y:] by A4, XBOOLE_0:def_10
.= dom f by A2, FUNCT_3:def_5 ;
A13: f is one-to-one by A2, Th5;
A14: f is onto by A3, FUNCT_2:def_3;
dom idZ = the carrier of Y by FUNCT_2:def_1
.= dom (id Y) by FUNCT_2:def_1 ;
then  f * KA = id (rng f) by A2, A3, A11, A1, FUNCT_3:52;
then  KA = f " by A13, A12, FUNCT_1:42;
hence  f " = <:(Y --> x),(id Y):> by A13, A14, TOPS_2:def_4; ::_thesis: verum
end;

theorem :: BORSUK_3:8
for X, Y being non empty TopSpace
for x being Point of X
for f being Function of [:Y,(X | {x}):],Y st f = pr1 ( the carrier of Y,{x}) holds
f is being_homeomorphism
proof
let X, Y be non empty TopSpace; ::_thesis: for x being Point of X
for f being Function of [:Y,(X | {x}):],Y st f = pr1 ( the carrier of Y,{x}) holds
f is being_homeomorphism
let x be Point of X; ::_thesis: for f being Function of [:Y,(X | {x}):],Y st f = pr1 ( the carrier of Y,{x}) holds
f is being_homeomorphism
let f be Function of [:Y,(X | {x}):],Y; ::_thesis: ( f = pr1 ( the carrier of Y,{x}) implies f is being_homeomorphism )
set Z = {x};
assume A1: f = pr1 ( the carrier of Y,{x}) ; ::_thesis: f is being_homeomorphism
thus  dom f = [#] [:Y,(X | {x}):] by FUNCT_2:def_1; :: according to TOPS_2:def_5 ::_thesis: ( rng f = [#] Y & f is one-to-one & f is continuous & f " is continuous )
thus  rng f = [#] Y by A1, FUNCT_3:44; ::_thesis: ( f is one-to-one & f is continuous & f " is continuous )
thus  f is one-to-one by A1, Th4; ::_thesis: ( f is continuous & f " is continuous )
 the carrier of (X | {x}) = {x} by PRE_TOPC:8;
hence  f is continuous by A1, YELLOW12:39; ::_thesis: f " is continuous
reconsider Z = {x} as non empty Subset of X ;
reconsider idZ = Y --> x as continuous Function of Y,(X | Z) by Th2;
reconsider KA = <:(id Y),idZ:> as continuous Function of Y,[:Y,(X | Z):] by YELLOW12:41;
 KA = f " by A1, Th6;
hence  f " is continuous ; ::_thesis: verum
end;

theorem Th9: :: BORSUK_3:9
for X, Y being non empty TopSpace
for x being Point of X
for f being Function of [:(X | {x}),Y:],Y st f = pr2 ({x}, the carrier of Y) holds
f is being_homeomorphism
proof
let X, Y be non empty TopSpace; ::_thesis: for x being Point of X
for f being Function of [:(X | {x}),Y:],Y st f = pr2 ({x}, the carrier of Y) holds
f is being_homeomorphism
let x be Point of X; ::_thesis: for f being Function of [:(X | {x}),Y:],Y st f = pr2 ({x}, the carrier of Y) holds
f is being_homeomorphism
let f be Function of [:(X | {x}),Y:],Y; ::_thesis: ( f = pr2 ({x}, the carrier of Y) implies f is being_homeomorphism )
set Z = {x};
assume A1: f = pr2 ({x}, the carrier of Y) ; ::_thesis: f is being_homeomorphism
thus  dom f = [#] [:(X | {x}),Y:] by FUNCT_2:def_1; :: according to TOPS_2:def_5 ::_thesis: ( rng f = [#] Y & f is one-to-one & f is continuous & f " is continuous )
thus  rng f = [#] Y by A1, FUNCT_3:46; ::_thesis: ( f is one-to-one & f is continuous & f " is continuous )
thus  f is one-to-one by A1, Th5; ::_thesis: ( f is continuous & f " is continuous )
 the carrier of (X | {x}) = {x} by PRE_TOPC:8;
hence  f is continuous by A1, YELLOW12:40; ::_thesis: f " is continuous
reconsider Z = {x} as non empty Subset of X ;
reconsider idZ = Y --> x as continuous Function of Y,(X | Z) by Th2;
reconsider KA = <:idZ,(id Y):> as continuous Function of Y,[:(X | Z),Y:] by YELLOW12:41;
 KA = f " by A1, Th7;
hence  f " is continuous ; ::_thesis: verum
end;

begin

theorem :: BORSUK_3:10
for X being non empty TopSpace
for Y being non empty compact TopSpace
for G being open Subset of [:X,Y:]
for x being set st [:{x}, the carrier of Y:] c= G holds
ex f being ManySortedSet of the carrier of Y st
for i being set st i in the carrier of Y holds
ex G1 being Subset of X ex H1 being Subset of Y st
( f . i = [G1,H1] & [x,i] in [:G1,H1:] & G1 is open & H1 is open & [:G1,H1:] c= G )
proof
let X be non empty TopSpace; ::_thesis: for Y being non empty compact TopSpace
for G being open Subset of [:X,Y:]
for x being set st [:{x}, the carrier of Y:] c= G holds
ex f being ManySortedSet of the carrier of Y st
for i being set st i in the carrier of Y holds
ex G1 being Subset of X ex H1 being Subset of Y st
( f . i = [G1,H1] & [x,i] in [:G1,H1:] & G1 is open & H1 is open & [:G1,H1:] c= G )
let Y be non empty compact TopSpace; ::_thesis: for G being open Subset of [:X,Y:]
for x being set st [:{x}, the carrier of Y:] c= G holds
ex f being ManySortedSet of the carrier of Y st
for i being set st i in the carrier of Y holds
ex G1 being Subset of X ex H1 being Subset of Y st
( f . i = [G1,H1] & [x,i] in [:G1,H1:] & G1 is open & H1 is open & [:G1,H1:] c= G )
let G be open Subset of [:X,Y:]; ::_thesis: for x being set st [:{x}, the carrier of Y:] c= G holds
ex f being ManySortedSet of the carrier of Y st
for i being set st i in the carrier of Y holds
ex G1 being Subset of X ex H1 being Subset of Y st
( f . i = [G1,H1] & [x,i] in [:G1,H1:] & G1 is open & H1 is open & [:G1,H1:] c= G )
let x be set ; ::_thesis: ( [:{x}, the carrier of Y:] c= G implies ex f being ManySortedSet of the carrier of Y st
for i being set st i in the carrier of Y holds
ex G1 being Subset of X ex H1 being Subset of Y st
( f . i = [G1,H1] & [x,i] in [:G1,H1:] & G1 is open & H1 is open & [:G1,H1:] c= G ) )
set y = the Point of Y;
A1: ( the carrier of [:X,Y:] = [: the carrier of X, the carrier of Y:] & [x, the Point of Y] in [:{x}, the carrier of Y:] ) by BORSUK_1:def_2, ZFMISC_1:105;
defpred S1[ set , set ] means  ex G1 being Subset of X ex H1 being Subset of Y st
( $2 = [G1,H1] & [x,$1] in [:G1,H1:] & G1 is open & H1 is open & [:G1,H1:] c= G );
assume A2: [:{x}, the carrier of Y:] c= G ; ::_thesis: ex f being ManySortedSet of the carrier of Y st
for i being set st i in the carrier of Y holds
ex G1 being Subset of X ex H1 being Subset of Y st
( f . i = [G1,H1] & [x,i] in [:G1,H1:] & G1 is open & H1 is open & [:G1,H1:] c= G )
then  [:{x}, the carrier of Y:] c= the carrier of [:X,Y:] by XBOOLE_1:1;
then reconsider x9 = x as Point of X by A1, ZFMISC_1:87;
A3: [:{x9}, the carrier of Y:] c= union (Base-Appr G) by A2, BORSUK_1:13;
A4: now__::_thesis:_for_y_being_set_st_y_in_the_carrier_of_Y_holds_
ex_G1_being_Subset_of_X_ex_H1_being_Subset_of_Y_st_
(_[x,y]_in_[:G1,H1:]_&_[:G1,H1:]_c=_G_&_G1_is_open_&_H1_is_open_)
let y be set ; ::_thesis: ( y in the carrier of Y implies ex G1 being Subset of X ex H1 being Subset of Y st
( [x,y] in [:G1,H1:] & [:G1,H1:] c= G & G1 is open & H1 is open ) )
A5: x in {x9} by TARSKI:def_1;
assume  y in the carrier of Y ; ::_thesis: ex G1 being Subset of X ex H1 being Subset of Y st
( [x,y] in [:G1,H1:] & [:G1,H1:] c= G & G1 is open & H1 is open )
then  [x,y] in [:{x9}, the carrier of Y:] by A5, ZFMISC_1:87;
then consider Z being set  such that
A6: [x,y] in Z and
A7: Z in Base-Appr G by A3, TARSKI:def_4;
 Base-Appr G =  {  [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( [:X1,Y1:] c= G & X1 is open & Y1 is open )  }  by BORSUK_1:def_3;
then  ex X1 being Subset of X ex Y1 being Subset of Y st
( Z = [:X1,Y1:] & [:X1,Y1:] c= G & X1 is open & Y1 is open ) by A7;
hence  ex G1 being Subset of X ex H1 being Subset of Y st
( [x,y] in [:G1,H1:] & [:G1,H1:] c= G & G1 is open & H1 is open ) by A6; ::_thesis: verum
end;
A8: for i being set st i in the carrier of Y holds
ex j being set st S1[i,j]
proof
let i be set ; ::_thesis: ( i in the carrier of Y implies ex j being set st S1[i,j] )
assume  i in the carrier of Y ; ::_thesis: ex j being set st S1[i,j]
then consider G1 being Subset of X, H1 being Subset of Y such that
A9: ( [x,i] in [:G1,H1:] & [:G1,H1:] c= G & G1 is open & H1 is open ) by A4;
 ex G2 being Subset of X ex H2 being Subset of Y st
( [G1,H1] = [G2,H2] & [x,i] in [:G2,H2:] & G2 is open & H2 is open & [:G2,H2:] c= G ) by A9;
hence  ex j being set st S1[i,j] ; ::_thesis: verum
end;
 ex f being ManySortedSet of the carrier of Y st
for i being set st i in the carrier of Y holds
S1[i,f . i] from PBOOLE:sch_3(A8);
hence  ex f being ManySortedSet of the carrier of Y st
for i being set st i in the carrier of Y holds
ex G1 being Subset of X ex H1 being Subset of Y st
( f . i = [G1,H1] & [x,i] in [:G1,H1:] & G1 is open & H1 is open & [:G1,H1:] c= G ) ; ::_thesis: verum
end;

theorem Th11: :: BORSUK_3:11
for X being non empty TopSpace
for Y being non empty compact TopSpace
for G being open Subset of [:Y,X:]
for x being set st [:([#] Y),{x}:] c= G holds
ex R being open Subset of X st
( x in R & R c=  {  y where y is Point of X : [:([#] Y),{y}:] c= G  }  )
proof
let X be non empty TopSpace; ::_thesis: for Y being non empty compact TopSpace
for G being open Subset of [:Y,X:]
for x being set st [:([#] Y),{x}:] c= G holds
ex R being open Subset of X st
( x in R & R c=  {  y where y is Point of X : [:([#] Y),{y}:] c= G  }  )
let Y be non empty compact TopSpace; ::_thesis: for G being open Subset of [:Y,X:]
for x being set st [:([#] Y),{x}:] c= G holds
ex R being open Subset of X st
( x in R & R c=  {  y where y is Point of X : [:([#] Y),{y}:] c= G  }  )
let G be open Subset of [:Y,X:]; ::_thesis: for x being set st [:([#] Y),{x}:] c= G holds
ex R being open Subset of X st
( x in R & R c=  {  y where y is Point of X : [:([#] Y),{y}:] c= G  }  )
let x be set ; ::_thesis: ( [:([#] Y),{x}:] c= G implies ex R being open Subset of X st
( x in R & R c=  {  y where y is Point of X : [:([#] Y),{y}:] c= G  }  ) )
set y = the Point of Y;
A1: ( the carrier of [:Y,X:] = [: the carrier of Y, the carrier of X:] & [ the Point of Y,x] in [: the carrier of Y,{x}:] ) by BORSUK_1:def_2, ZFMISC_1:106;
assume A2: [:([#] Y),{x}:] c= G ; ::_thesis: ex R being open Subset of X st
( x in R & R c=  {  y where y is Point of X : [:([#] Y),{y}:] c= G  }  )
then  [:([#] Y),{x}:] c= the carrier of [:Y,X:] by XBOOLE_1:1;
then reconsider x9 = x as Point of X by A1, ZFMISC_1:87;
 Int G = G by TOPS_1:23;
then  ( [#] Y is compact & G is a_neighborhood of [:([#] Y),{x9}:] ) by A2, COMPTS_1:1, CONNSP_2:def_2;
then consider W being a_neighborhood of [#] Y, V being a_neighborhood of x9 such that
A3: [:W,V:] c= G by BORSUK_1:25;
take R = Int V; ::_thesis: ( x in R & R c=  {  y where y is Point of X : [:([#] Y),{y}:] c= G  }  )
 ( Int W c= W & [#] Y c= Int W ) by CONNSP_2:def_2, TOPS_1:16;
then A4: [#] Y c= W by XBOOLE_1:1;
A5: Int V c= V by TOPS_1:16;
 R c=  {  z where z is Point of X : [:([#] Y),{z}:] c= G  }
proof
let r be set ; :: according to TARSKI:def_3 ::_thesis: ( not r in R or r in  {  z where z is Point of X : [:([#] Y),{z}:] c= G  }  )
assume A6: r in R ; ::_thesis: r in  {  z where z is Point of X : [:([#] Y),{z}:] c= G  }
then reconsider r9 = r as Point of X ;
 {r} c= V by A5, A6, ZFMISC_1:31;
then  [:([#] Y),{r9}:] c= [:W,V:] by A4, ZFMISC_1:96;
then  [:([#] Y),{r9}:] c= G by A3, XBOOLE_1:1;
hence  r in  {  z where z is Point of X : [:([#] Y),{z}:] c= G  }  ; ::_thesis: verum
end;
hence  ( x in R & R c=  {  y where y is Point of X : [:([#] Y),{y}:] c= G  }  ) by CONNSP_2:def_1; ::_thesis: verum
end;

theorem Th12: :: BORSUK_3:12
for X being non empty TopSpace
for Y being non empty compact TopSpace
for G being open Subset of [:Y,X:] holds  {  x where x is Point of X : [:([#] Y),{x}:] c= G  }  in the topology of X
proof
let X be non empty TopSpace; ::_thesis: for Y being non empty compact TopSpace
for G being open Subset of [:Y,X:] holds  {  x where x is Point of X : [:([#] Y),{x}:] c= G  }  in the topology of X
let Y be non empty compact TopSpace; ::_thesis: for G being open Subset of [:Y,X:] holds  {  x where x is Point of X : [:([#] Y),{x}:] c= G  }  in the topology of X
let G be open Subset of [:Y,X:]; ::_thesis:  {  x where x is Point of X : [:([#] Y),{x}:] c= G  }  in the topology of X
set Q =  {  x where x is Point of X : [:([#] Y),{x}:] c= G  }  ;
  {  x where x is Point of X : [:([#] Y),{x}:] c= G  }  c= the carrier of X
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in  {  x where x is Point of X : [:([#] Y),{x}:] c= G  }  or q in the carrier of X )
assume  q in  {  x where x is Point of X : [:([#] Y),{x}:] c= G  }  ; ::_thesis: q in the carrier of X
then  ex x9 being Point of X st
( q = x9 & [:([#] Y),{x9}:] c= G ) ;
hence  q in the carrier of X ; ::_thesis: verum
end;
then reconsider Q =  {  x where x is Point of X : [:([#] Y),{x}:] c= G  }  as Subset of X ;
defpred S1[ set ] means  ex y being set st
( y in Q & ex S being Subset of X st
( S = $1 & S is open & y in S & S c= Q ) );
consider RR being set  such that
A1: for x being set holds
( x in RR iff ( x in bool Q & S1[x] ) ) from XBOOLE_0:sch_1();
 RR c= bool Q
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in RR or x in bool Q )
assume  x in RR ; ::_thesis: x in bool Q
hence  x in bool Q by A1; ::_thesis: verum
end;
then reconsider RR = RR as Subset-Family of Q ;
 Q c= union RR
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in Q or a in union RR )
assume  a in Q ; ::_thesis: a in union RR
then  ex x9 being Point of X st
( a = x9 & [:([#] Y),{x9}:] c= G ) ;
then consider R being open Subset of X such that
A2: a in R and
A3: R c= Q by Th11;
 R in RR by A1, A2, A3;
hence  a in union RR by A2, TARSKI:def_4; ::_thesis: verum
end;
then A4: union RR = Q by XBOOLE_0:def_10;
 bool Q c= bool the carrier of X by ZFMISC_1:67;
then reconsider RR = RR as Subset-Family of X by XBOOLE_1:1;
 RR c= the topology of X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in RR or x in the topology of X )
assume  x in RR ; ::_thesis: x in the topology of X
then  ex y being set st
( y in Q & ex S being Subset of X st
( S = x & S is open & y in S & S c= Q ) ) by A1;
hence  x in the topology of X by PRE_TOPC:def_2; ::_thesis: verum
end;
hence   {  x where x is Point of X : [:([#] Y),{x}:] c= G  }  in the topology of X by A4, PRE_TOPC:def_1; ::_thesis: verum
end;

theorem Th13: :: BORSUK_3:13
for X, Y being non empty TopSpace
for x being Point of X holds [:(X | {x}),Y:],Y are_homeomorphic
proof
let X, Y be non empty TopSpace; ::_thesis: for x being Point of X holds [:(X | {x}),Y:],Y are_homeomorphic
let x be Point of X; ::_thesis: [:(X | {x}),Y:],Y are_homeomorphic
set Z = {x};
the carrier of [:(X | {x}),Y:] = [: the carrier of (X | {x}), the carrier of Y:] by BORSUK_1:def_2
.= [:{x}, the carrier of Y:] by PRE_TOPC:8 ;
then reconsider f = pr2 ({x}, the carrier of Y) as Function of [:(X | {x}),Y:],Y ;
take  f ; :: according to T_0TOPSP:def_1 ::_thesis: f is being_homeomorphism
thus  f is being_homeomorphism by Th9; ::_thesis: verum
end;

Lm3:  for X, Y being non empty TopSpace
for x being Point of X
for Z being non empty Subset of X st Z = {x} holds
[:Y,(X | Z):],Y are_homeomorphic
proof
let X, Y be non empty TopSpace; ::_thesis: for x being Point of X
for Z being non empty Subset of X st Z = {x} holds
[:Y,(X | Z):],Y are_homeomorphic
let x be Point of X; ::_thesis: for Z being non empty Subset of X st Z = {x} holds
[:Y,(X | Z):],Y are_homeomorphic
let Z be non empty Subset of X; ::_thesis: ( Z = {x} implies [:Y,(X | Z):],Y are_homeomorphic )
 [:Y,(X | Z):],[:(X | Z),Y:] are_homeomorphic by YELLOW12:44;
then consider g being Function of [:Y,(X | Z):],[:(X | Z),Y:] such that
A1: g is being_homeomorphism by T_0TOPSP:def_1;
assume  Z = {x} ; ::_thesis: [:Y,(X | Z):],Y are_homeomorphic
then  [:(X | Z),Y:],Y are_homeomorphic by Th13;
then consider f being Function of [:(X | Z),Y:],Y such that
A2: f is being_homeomorphism by T_0TOPSP:def_1;
reconsider gf = f * g as Function of [:Y,(X | Z):],Y ;
 gf is being_homeomorphism by A2, A1, TOPS_2:57;
hence  [:Y,(X | Z):],Y are_homeomorphic by T_0TOPSP:def_1; ::_thesis: verum
end;

theorem Th14: :: BORSUK_3:14
for S, T being non empty TopSpace st S,T are_homeomorphic & S is compact holds
T is compact
proof
let S, T be non empty TopSpace; ::_thesis: ( S,T are_homeomorphic & S is compact implies T is compact )
assume that
A1: S,T are_homeomorphic and
A2: S is compact ; ::_thesis: T is compact
consider f being Function of S,T such that
A3: f is being_homeomorphism by A1, T_0TOPSP:def_1;
 ( f is continuous & rng f = [#] T ) by A3, TOPS_2:def_5;
hence  T is compact by A2, COMPTS_1:14; ::_thesis: verum
end;

theorem Th15: :: BORSUK_3:15
for X, Y being TopSpace
for XV being SubSpace of X holds [:Y,XV:] is SubSpace of [:Y,X:]
proof
let X, Y be TopSpace; ::_thesis: for XV being SubSpace of X holds [:Y,XV:] is SubSpace of [:Y,X:]
let XV be SubSpace of X; ::_thesis: [:Y,XV:] is SubSpace of [:Y,X:]
set S = [:Y,XV:];
set T = [:Y,X:];
A1: the carrier of [:Y,XV:] = [: the carrier of Y, the carrier of XV:] by BORSUK_1:def_2;
A2: ( the carrier of [:Y,X:] = [: the carrier of Y, the carrier of X:] & the carrier of XV c= the carrier of X ) by BORSUK_1:1, BORSUK_1:def_2;
A3: for P being Subset of [:Y,XV:] holds
( P in the topology of [:Y,XV:] iff ex Q being Subset of [:Y,X:] st
( Q in the topology of [:Y,X:] & P = Q /\ ([#] [:Y,XV:]) ) )
proof
reconsider oS = [#] [:Y,XV:] as Subset of [:Y,X:] by A1, A2, ZFMISC_1:96;
let P be Subset of [:Y,XV:]; ::_thesis: ( P in the topology of [:Y,XV:] iff ex Q being Subset of [:Y,X:] st
( Q in the topology of [:Y,X:] & P = Q /\ ([#] [:Y,XV:]) ) )
reconsider P9 = P as Subset of [:Y,XV:] ;
hereby  ::_thesis: ( ex Q being Subset of [:Y,X:] st
( Q in the topology of [:Y,X:] & P = Q /\ ([#] [:Y,XV:]) ) implies P in the topology of [:Y,XV:] )
assume  P in the topology of [:Y,XV:] ; ::_thesis: ex Q being Subset of [:Y,X:] st
( Q in the topology of [:Y,X:] & P = Q /\ ([#] [:Y,XV:]) )
then  P9 is open by PRE_TOPC:def_2;
then consider A being Subset-Family of [:Y,XV:] such that
A4: P9 = union A and
A5: for e being set st e in A holds
ex X1 being Subset of Y ex Y1 being Subset of XV st
( e = [:X1,Y1:] & X1 is open & Y1 is open ) by BORSUK_1:5;
set AA =  {  [:X1,Y2:] where X1 is Subset of Y, Y2 is Subset of X : ex Y1 being Subset of XV st
( Y1 = Y2 /\ ([#] XV) & X1 is open & Y2 is open & [:X1,Y1:] in A )  }  ;
  {  [:X1,Y2:] where X1 is Subset of Y, Y2 is Subset of X : ex Y1 being Subset of XV st
( Y1 = Y2 /\ ([#] XV) & X1 is open & Y2 is open & [:X1,Y1:] in A )  }  c= bool the carrier of [:Y,X:]
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in  {  [:X1,Y2:] where X1 is Subset of Y, Y2 is Subset of X : ex Y1 being Subset of XV st
( Y1 = Y2 /\ ([#] XV) & X1 is open & Y2 is open & [:X1,Y1:] in A )  }  or a in bool the carrier of [:Y,X:] )
assume  a in  {  [:X1,Y2:] where X1 is Subset of Y, Y2 is Subset of X : ex Y1 being Subset of XV st
( Y1 = Y2 /\ ([#] XV) & X1 is open & Y2 is open & [:X1,Y1:] in A )  }  ; ::_thesis: a in bool the carrier of [:Y,X:]
then  ex Xx1 being Subset of Y ex Yy2 being Subset of X st
( a = [:Xx1,Yy2:] & ex Y1 being Subset of XV st
( Y1 = Yy2 /\ ([#] XV) & Xx1 is open & Yy2 is open & [:Xx1,Y1:] in A ) ) ;
hence  a in bool the carrier of [:Y,X:] ; ::_thesis: verum
end;
then reconsider AA =  {  [:X1,Y2:] where X1 is Subset of Y, Y2 is Subset of X : ex Y1 being Subset of XV st
( Y1 = Y2 /\ ([#] XV) & X1 is open & Y2 is open & [:X1,Y1:] in A )  }  as Subset-Family of [:Y,X:] ;
reconsider AA = AA as Subset-Family of [:Y,X:] ;
A6: P c= (union AA) /\ ([#] [:Y,XV:])
proof
let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in P or p in (union AA) /\ ([#] [:Y,XV:]) )
assume  p in P ; ::_thesis: p in (union AA) /\ ([#] [:Y,XV:])
then consider A1 being set  such that
A7: p in A1 and
A8: A1 in A by A4, TARSKI:def_4;
reconsider A1 = A1 as Subset of [:Y,XV:] by A8;
consider X2 being Subset of Y, Y2 being Subset of XV such that
A9: A1 = [:X2,Y2:] and
A10: X2 is open and
A11: Y2 is open by A5, A8;
 Y2 in the topology of XV by A11, PRE_TOPC:def_2;
then consider Q1 being Subset of X such that
A12: Q1 in the topology of X and
A13: Y2 = Q1 /\ ([#] XV) by PRE_TOPC:def_4;
consider p1, p2 being set  such that
A14: p1 in X2 and
A15: p2 in Y2 and
A16: p = [p1,p2] by A7, A9, ZFMISC_1:def_2;
reconsider Q1 = Q1 as Subset of X ;
set EX = [:X2,Q1:];
 p2 in Q1 by A15, A13, XBOOLE_0:def_4;
then A17: p in [:X2,Q1:] by A14, A16, ZFMISC_1:87;
 Q1 is open by A12, PRE_TOPC:def_2;
then  [:X2,Q1:] in  {  [:Xx1,Yy2:] where Xx1 is Subset of Y, Yy2 is Subset of X : ex Z1 being Subset of XV st
( Z1 = Yy2 /\ ([#] XV) & Xx1 is open & Yy2 is open & [:Xx1,Z1:] in A )  }  by A8, A9, A10, A13;
then  p in union AA by A17, TARSKI:def_4;
hence  p in (union AA) /\ ([#] [:Y,XV:]) by A7, A8, XBOOLE_0:def_4; ::_thesis: verum
end;
 AA c= the topology of [:Y,X:]
proof
let t be set ; :: according to TARSKI:def_3 ::_thesis: ( not t in AA or t in the topology of [:Y,X:] )
set A9 = {t};
assume  t in AA ; ::_thesis: t in the topology of [:Y,X:]
then consider Xx1 being Subset of Y, Yy2 being Subset of X such that
A18: t = [:Xx1,Yy2:] and
A19: ex Y1 being Subset of XV st
( Y1 = Yy2 /\ ([#] XV) & Xx1 is open & Yy2 is open & [:Xx1,Y1:] in A ) ;
 {t} c= bool the carrier of [:Y,X:]
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in {t} or a in bool the carrier of [:Y,X:] )
assume  a in {t} ; ::_thesis: a in bool the carrier of [:Y,X:]
then  a = t by TARSKI:def_1;
hence  a in bool the carrier of [:Y,X:] by A18; ::_thesis: verum
end;
then reconsider A9 = {t} as Subset-Family of [:Y,X:] ;
A20: A9 c=  {  [:X1,Y1:] where X1 is Subset of Y, Y1 is Subset of X : ( X1 in the topology of Y & Y1 in the topology of X )  }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A9 or x in  {  [:X1,Y1:] where X1 is Subset of Y, Y1 is Subset of X : ( X1 in the topology of Y & Y1 in the topology of X )  }  )
assume  x in A9 ; ::_thesis: x in  {  [:X1,Y1:] where X1 is Subset of Y, Y1 is Subset of X : ( X1 in the topology of Y & Y1 in the topology of X )  }
then A21: x = [:Xx1,Yy2:] by A18, TARSKI:def_1;
 ( Xx1 in the topology of Y & Yy2 in the topology of X ) by A19, PRE_TOPC:def_2;
hence  x in  {  [:X1,Y1:] where X1 is Subset of Y, Y1 is Subset of X : ( X1 in the topology of Y & Y1 in the topology of X )  }  by A21; ::_thesis: verum
end;
 t = union A9 by ZFMISC_1:25;
then  t in  {  (union As) where As is Subset-Family of [:Y,X:] : As c=  {  [:X1,Y1:] where X1 is Subset of Y, Y1 is Subset of X : ( X1 in the topology of Y & Y1 in the topology of X )  }   }  by A20;
hence  t in the topology of [:Y,X:] by BORSUK_1:def_2; ::_thesis: verum
end;
then A22: union AA in the topology of [:Y,X:] by PRE_TOPC:def_1;
 (union AA) /\ ([#] [:Y,XV:]) c= P
proof
let h be set ; :: according to TARSKI:def_3 ::_thesis: ( not h in (union AA) /\ ([#] [:Y,XV:]) or h in P )
assume A23: h in (union AA) /\ ([#] [:Y,XV:]) ; ::_thesis: h in P
then  h in union AA by XBOOLE_0:def_4;
then consider A2 being set  such that
A24: h in A2 and
A25: A2 in AA by TARSKI:def_4;
consider Xx1 being Subset of Y, Yy2 being Subset of X such that
A26: A2 = [:Xx1,Yy2:] and
A27: ex Y1 being Subset of XV st
( Y1 = Yy2 /\ ([#] XV) & Xx1 is open & Yy2 is open & [:Xx1,Y1:] in A ) by A25;
consider Yy1 being Subset of XV such that
A28: Yy1 = Yy2 /\ ([#] XV) and
 Xx1 is open and
 Yy2 is open and
A29: [:Xx1,Yy1:] in A by A27;
consider p1, p2 being set  such that
A30: p1 in Xx1 and
A31: p2 in Yy2 and
A32: h = [p1,p2] by A24, A26, ZFMISC_1:def_2;
 p2 in the carrier of XV by A1, A23, A32, ZFMISC_1:87;
then  p2 in Yy2 /\ ([#] XV) by A31, XBOOLE_0:def_4;
then  h in [:Xx1,Yy1:] by A30, A32, A28, ZFMISC_1:87;
hence  h in P by A4, A29, TARSKI:def_4; ::_thesis: verum
end;
then  P = (union AA) /\ ([#] [:Y,XV:]) by A6, XBOOLE_0:def_10;
hence  ex Q being Subset of [:Y,X:] st
( Q in the topology of [:Y,X:] & P = Q /\ ([#] [:Y,XV:]) ) by A22; ::_thesis: verum
end;
given Q being Subset of [:Y,X:] such that A33: Q in the topology of [:Y,X:] and
A34: P = Q /\ ([#] [:Y,XV:]) ; ::_thesis: P in the topology of [:Y,XV:]
reconsider Q9 = Q as Subset of [:Y,X:] ;
 Q9 is open by A33, PRE_TOPC:def_2;
then consider A being Subset-Family of [:Y,X:] such that
A35: Q9 = union A and
A36: for e being set st e in A holds
ex X1 being Subset of Y ex Y1 being Subset of X st
( e = [:X1,Y1:] & X1 is open & Y1 is open ) by BORSUK_1:5;
reconsider A = A as Subset-Family of [:Y,X:] ;
reconsider AA = A | oS as Subset-Family of ([:Y,X:] | oS) ;
reconsider AA = AA as Subset-Family of [:Y,XV:] by PRE_TOPC:8;
reconsider AA = AA as Subset-Family of [:Y,XV:] ;
A37: for e being set st e in AA holds
ex X1 being Subset of Y ex Y1 being Subset of XV st
( e = [:X1,Y1:] & X1 is open & Y1 is open )
proof
let e be set ; ::_thesis: ( e in AA implies ex X1 being Subset of Y ex Y1 being Subset of XV st
( e = [:X1,Y1:] & X1 is open & Y1 is open ) )
assume A38: e in AA ; ::_thesis: ex X1 being Subset of Y ex Y1 being Subset of XV st
( e = [:X1,Y1:] & X1 is open & Y1 is open )
then reconsider e9 = e as Subset of ([:Y,X:] | oS) ;
consider R being Subset of [:Y,X:] such that
A39: R in A and
A40: R /\ oS = e9 by A38, TOPS_2:def_3;
consider X1 being Subset of Y, Y1 being Subset of X such that
A41: R = [:X1,Y1:] and
A42: X1 is open and
A43: Y1 is open by A36, A39;
reconsider D2 = Y1 /\ ([#] XV) as Subset of XV ;
 Y1 in the topology of X by A43, PRE_TOPC:def_2;
then  D2 in the topology of XV by PRE_TOPC:def_4;
then A44: D2 is open by PRE_TOPC:def_2;
 [#] [:Y,XV:] = [:([#] Y),([#] XV):] by BORSUK_1:def_2;
then  e9 = [:(X1 /\ ([#] Y)),(Y1 /\ ([#] XV)):] by A40, A41, ZFMISC_1:100;
hence  ex X1 being Subset of Y ex Y1 being Subset of XV st
( e = [:X1,Y1:] & X1 is open & Y1 is open ) by A42, A44; ::_thesis: verum
end;
A45: (union A) /\ oS c= union AA
proof
let s be set ; :: according to TARSKI:def_3 ::_thesis: ( not s in (union A) /\ oS or s in union AA )
assume A46: s in (union A) /\ oS ; ::_thesis: s in union AA
then  s in union A by XBOOLE_0:def_4;
then consider A1 being set  such that
A47: s in A1 and
A48: A1 in A by TARSKI:def_4;
 s in oS by A46, XBOOLE_0:def_4;
then A49: s in A1 /\ oS by A47, XBOOLE_0:def_4;
reconsider A1 = A1 as Subset of [:Y,X:] by A48;
 A1 /\ oS in AA by A48, TOPS_2:31;
hence  s in union AA by A49, TARSKI:def_4; ::_thesis: verum
end;
 union AA c= union A by TOPS_2:34;
then  union AA c= (union A) /\ oS by XBOOLE_1:19;
then  P = union AA by A34, A35, A45, XBOOLE_0:def_10;
then  P9 is open by A37, BORSUK_1:5;
hence  P in the topology of [:Y,XV:] by PRE_TOPC:def_2; ::_thesis: verum
end;
 [#] [:Y,XV:] c= [#] [:Y,X:] by A1, A2, ZFMISC_1:96;
hence  [:Y,XV:] is SubSpace of [:Y,X:] by A3, PRE_TOPC:def_4; ::_thesis: verum
end;

Lm4:  for X, Y being TopSpace
for Z being Subset of [:Y,X:]
for V being Subset of X st Z = [:([#] Y),V:] holds
TopStruct(# the carrier of [:Y,(X | V):], the topology of [:Y,(X | V):] #) = TopStruct(# the carrier of ([:Y,X:] | Z), the topology of ([:Y,X:] | Z) #)
proof
let X, Y be TopSpace; ::_thesis: for Z being Subset of [:Y,X:]
for V being Subset of X st Z = [:([#] Y),V:] holds
TopStruct(# the carrier of [:Y,(X | V):], the topology of [:Y,(X | V):] #) = TopStruct(# the carrier of ([:Y,X:] | Z), the topology of ([:Y,X:] | Z) #)
let Z be Subset of [:Y,X:]; ::_thesis: for V being Subset of X st Z = [:([#] Y),V:] holds
TopStruct(# the carrier of [:Y,(X | V):], the topology of [:Y,(X | V):] #) = TopStruct(# the carrier of ([:Y,X:] | Z), the topology of ([:Y,X:] | Z) #)
let V be Subset of X; ::_thesis: ( Z = [:([#] Y),V:] implies TopStruct(# the carrier of [:Y,(X | V):], the topology of [:Y,(X | V):] #) = TopStruct(# the carrier of ([:Y,X:] | Z), the topology of ([:Y,X:] | Z) #) )
reconsider A = [:Y,(X | V):] as SubSpace of [:Y,X:] by Th15;
assume A1: Z = [:([#] Y),V:] ; ::_thesis: TopStruct(# the carrier of [:Y,(X | V):], the topology of [:Y,(X | V):] #) = TopStruct(# the carrier of ([:Y,X:] | Z), the topology of ([:Y,X:] | Z) #)
the carrier of A = [: the carrier of Y, the carrier of (X | V):] by BORSUK_1:def_2
.= Z by A1, PRE_TOPC:8
.= the carrier of ([:Y,X:] | Z) by PRE_TOPC:8 ;
then  ( A is SubSpace of [:Y,X:] | Z & [:Y,X:] | Z is SubSpace of A ) by TOPMETR:3;
hence  TopStruct(# the carrier of [:Y,(X | V):], the topology of [:Y,(X | V):] #) = TopStruct(# the carrier of ([:Y,X:] | Z), the topology of ([:Y,X:] | Z) #) by TSEP_1:6; ::_thesis: verum
end;

theorem Th16: :: BORSUK_3:16
for X being non empty TopSpace
for Y being non empty compact TopSpace
for x being Point of X
for Z being Subset of [:Y,X:] st Z = [:([#] Y),{x}:] holds
Z is compact
proof
let X be non empty TopSpace; ::_thesis: for Y being non empty compact TopSpace
for x being Point of X
for Z being Subset of [:Y,X:] st Z = [:([#] Y),{x}:] holds
Z is compact
let Y be non empty compact TopSpace; ::_thesis: for x being Point of X
for Z being Subset of [:Y,X:] st Z = [:([#] Y),{x}:] holds
Z is compact
let x be Point of X; ::_thesis: for Z being Subset of [:Y,X:] st Z = [:([#] Y),{x}:] holds
Z is compact
let Z be Subset of [:Y,X:]; ::_thesis: ( Z = [:([#] Y),{x}:] implies Z is compact )
reconsider V = {x} as non empty Subset of X ;
 Y,[:Y,(X | V):] are_homeomorphic by Lm3;
then A1: [:Y,(X | V):] is compact by Th14;
assume A2: Z = [:([#] Y),{x}:] ; ::_thesis: Z is compact
then  TopStruct(# the carrier of [:Y,(X | V):], the topology of [:Y,(X | V):] #) = TopStruct(# the carrier of ([:Y,X:] | Z), the topology of ([:Y,X:] | Z) #) by Lm4;
hence  Z is compact by A2, A1, COMPTS_1:3; ::_thesis: verum
end;

registration
let X be non empty TopSpace;
let Y be non empty compact TopSpace;
let x be Point of X;
cluster[:Y,(X | {x}):] ->  compact ;
coherence
 [:Y,(X | {x}):] is compact
proof
 Y,[:Y,(X | {x}):] are_homeomorphic by Lm3;
hence  [:Y,(X | {x}):] is compact by Th14; ::_thesis: verum
end;
end;

theorem :: BORSUK_3:17
for X, Y being non empty compact TopSpace
for R being Subset-Family of X st R =  {  Q where Q is open Subset of X : [:([#] Y),Q:] c= union (Base-Appr ([#] [:Y,X:]))  }  holds
( R is open & R is Cover of [#] X )
proof
let X, Y be non empty compact TopSpace; ::_thesis: for R being Subset-Family of X st R =  {  Q where Q is open Subset of X : [:([#] Y),Q:] c= union (Base-Appr ([#] [:Y,X:]))  }  holds
( R is open & R is Cover of [#] X )
let R be Subset-Family of X; ::_thesis: ( R =  {  Q where Q is open Subset of X : [:([#] Y),Q:] c= union (Base-Appr ([#] [:Y,X:]))  }  implies ( R is open & R is Cover of [#] X ) )
assume A1: R =  {  Q where Q is open Subset of X : [:([#] Y),Q:] c= union (Base-Appr ([#] [:Y,X:]))  }  ; ::_thesis: ( R is open & R is Cover of [#] X )
now__::_thesis:_for_P_being_Subset_of_X_st_P_in_R_holds_
P_is_open
let P be Subset of X; ::_thesis: ( P in R implies P is open )
assume  P in R ; ::_thesis: P is open
then  ex E being open Subset of X st
( E = P & [:([#] Y),E:] c= union (Base-Appr ([#] [:Y,X:])) ) by A1;
hence  P is open ; ::_thesis: verum
end;
hence  R is open by TOPS_2:def_1; ::_thesis: R is Cover of [#] X
 [#] X c= union R
proof
let k be set ; :: according to TARSKI:def_3 ::_thesis: ( not k in [#] X or k in union R )
assume  k in [#] X ; ::_thesis: k in union R
then reconsider k9 = k as Point of X ;
reconsider Z = [:([#] Y),{k9}:] as Subset of [:Y,X:] ;
 Z c= [#] [:Y,X:] ;
then  Z c= union (Base-Appr ([#] [:Y,X:])) by BORSUK_1:13;
then A2: Base-Appr ([#] [:Y,X:]) is Cover of Z by SETFAM_1:def_11;
 Z is compact by Th16;
then consider G being Subset-Family of [:Y,X:] such that
A3: G c= Base-Appr ([#] [:Y,X:]) and
A4: G is Cover of Z and
 G is finite by A2, COMPTS_1:def_4;
set uR = union G;
set Q =  {  x where x is Point of X : [:([#] Y),{x}:] c= union G  }  ;
  {  x where x is Point of X : [:([#] Y),{x}:] c= union G  }  c= the carrier of X
proof
let k be set ; :: according to TARSKI:def_3 ::_thesis: ( not k in  {  x where x is Point of X : [:([#] Y),{x}:] c= union G  }  or k in the carrier of X )
assume  k in  {  x where x is Point of X : [:([#] Y),{x}:] c= union G  }  ; ::_thesis: k in the carrier of X
then  ex x1 being Point of X st
( k = x1 & [:([#] Y),{x1}:] c= union G ) ;
hence  k in the carrier of X ; ::_thesis: verum
end;
then reconsider Q =  {  x where x is Point of X : [:([#] Y),{x}:] c= union G  }  as Subset of X ;
 Z c= union G by A4, SETFAM_1:def_11;
then A5: k9 in Q ;
A6: [:([#] Y),Q:] c= union (Base-Appr ([#] [:Y,X:]))
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in [:([#] Y),Q:] or z in union (Base-Appr ([#] [:Y,X:])) )
assume  z in [:([#] Y),Q:] ; ::_thesis: z in union (Base-Appr ([#] [:Y,X:]))
then consider x1, x2 being set  such that
A7: x1 in [#] Y and
A8: x2 in Q and
A9: z = [x1,x2] by ZFMISC_1:def_2;
consider x29 being Point of X such that
A10: x29 = x2 and
A11: [:([#] Y),{x29}:] c= union G by A8;
 x2 in {x29} by A10, TARSKI:def_1;
then A12: z in [:([#] Y),{x29}:] by A7, A9, ZFMISC_1:87;
 union G c= union (Base-Appr ([#] [:Y,X:])) by A3, ZFMISC_1:77;
then  [:([#] Y),{x29}:] c= union (Base-Appr ([#] [:Y,X:])) by A11, XBOOLE_1:1;
hence  z in union (Base-Appr ([#] [:Y,X:])) by A12; ::_thesis: verum
end;
 union G is open by A3, TOPS_2:11, TOPS_2:19;
then  Q in the topology of X by Th12;
then  Q is open by PRE_TOPC:def_2;
then  Q in R by A1, A6;
hence  k in union R by A5, TARSKI:def_4; ::_thesis: verum
end;
hence  R is Cover of [#] X by SETFAM_1:def_11; ::_thesis: verum
end;

theorem Th18: :: BORSUK_3:18
for X, Y being non empty compact TopSpace
for R being Subset-Family of X
for F being Subset-Family of [:Y,X:] st F is Cover of [:Y,X:] & F is open & R =  {  Q where Q is open Subset of X : ex FQ being Subset-Family of [:Y,X:] st
( FQ c= F & FQ is finite & [:([#] Y),Q:] c= union FQ )  }  holds
( R is open & R is Cover of X )
proof
let X, Y be non empty compact TopSpace; ::_thesis: for R being Subset-Family of X
for F being Subset-Family of [:Y,X:] st F is Cover of [:Y,X:] & F is open & R =  {  Q where Q is open Subset of X : ex FQ being Subset-Family of [:Y,X:] st
( FQ c= F & FQ is finite & [:([#] Y),Q:] c= union FQ )  }  holds
( R is open & R is Cover of X )
let R be Subset-Family of X; ::_thesis: for F being Subset-Family of [:Y,X:] st F is Cover of [:Y,X:] & F is open & R =  {  Q where Q is open Subset of X : ex FQ being Subset-Family of [:Y,X:] st
( FQ c= F & FQ is finite & [:([#] Y),Q:] c= union FQ )  }  holds
( R is open & R is Cover of X )
let F be Subset-Family of [:Y,X:]; ::_thesis: ( F is Cover of [:Y,X:] & F is open & R =  {  Q where Q is open Subset of X : ex FQ being Subset-Family of [:Y,X:] st
( FQ c= F & FQ is finite & [:([#] Y),Q:] c= union FQ )  }  implies ( R is open & R is Cover of X ) )
assume that
A1: F is Cover of [:Y,X:] and
A2: F is open and
A3: R =  {  Q where Q is open Subset of X : ex FQ being Subset-Family of [:Y,X:] st
( FQ c= F & FQ is finite & [:([#] Y),Q:] c= union FQ )  }  ; ::_thesis: ( R is open & R is Cover of X )
now__::_thesis:_for_P_being_Subset_of_X_st_P_in_R_holds_
P_is_open
let P be Subset of X; ::_thesis: ( P in R implies P is open )
assume  P in R ; ::_thesis: P is open
then  ex E being open Subset of X st
( E = P & ex FQ being Subset-Family of [:Y,X:] st
( FQ c= F & FQ is finite & [:([#] Y),E:] c= union FQ ) ) by A3;
hence  P is open ; ::_thesis: verum
end;
hence  R is open by TOPS_2:def_1; ::_thesis: R is Cover of X
A4: union F = [#] [:Y,X:] by A1, SETFAM_1:45;
 [#] X c= union R
proof
let k be set ; :: according to TARSKI:def_3 ::_thesis: ( not k in [#] X or k in union R )
assume  k in [#] X ; ::_thesis: k in union R
then reconsider k9 = k as Point of X ;
reconsider Z = [:([#] Y),{k9}:] as Subset of [:Y,X:] ;
 ( F is Cover of Z & Z is compact ) by A4, Th16, SETFAM_1:def_11;
then consider G being Subset-Family of [:Y,X:] such that
A5: G c= F and
A6: G is Cover of Z and
A7: G is finite by A2, COMPTS_1:def_4;
set uR = union G;
set Q =  {  x where x is Point of X : [:([#] Y),{x}:] c= union G  }  ;
  {  x where x is Point of X : [:([#] Y),{x}:] c= union G  }  c= the carrier of X
proof
let k be set ; :: according to TARSKI:def_3 ::_thesis: ( not k in  {  x where x is Point of X : [:([#] Y),{x}:] c= union G  }  or k in the carrier of X )
assume  k in  {  x where x is Point of X : [:([#] Y),{x}:] c= union G  }  ; ::_thesis: k in the carrier of X
then  ex x1 being Point of X st
( k = x1 & [:([#] Y),{x1}:] c= union G ) ;
hence  k in the carrier of X ; ::_thesis: verum
end;
then reconsider Q =  {  x where x is Point of X : [:([#] Y),{x}:] c= union G  }  as Subset of X ;
 Z c= union G by A6, SETFAM_1:def_11;
then A8: k9 in Q ;
A9: ex FQ being Subset-Family of [:Y,X:] st
( FQ c= F & FQ is finite & [:([#] Y),Q:] c= union FQ )
proof
take  G ; ::_thesis: ( G c= F & G is finite & [:([#] Y),Q:] c= union G )
 [:([#] Y),Q:] c= union G
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in [:([#] Y),Q:] or z in union G )
assume  z in [:([#] Y),Q:] ; ::_thesis: z in union G
then consider x1, x2 being set  such that
A10: x1 in [#] Y and
A11: x2 in Q and
A12: z = [x1,x2] by ZFMISC_1:def_2;
consider x29 being Point of X such that
A13: x29 = x2 and
A14: [:([#] Y),{x29}:] c= union G by A11;
 x2 in {x29} by A13, TARSKI:def_1;
then  z in [:([#] Y),{x29}:] by A10, A12, ZFMISC_1:87;
hence  z in union G by A14; ::_thesis: verum
end;
hence  ( G c= F & G is finite & [:([#] Y),Q:] c= union G ) by A5, A7; ::_thesis: verum
end;
 union G is open by A2, A5, TOPS_2:11, TOPS_2:19;
then  Q in the topology of X by Th12;
then  Q is open by PRE_TOPC:def_2;
then  Q in R by A3, A9;
hence  k in union R by A8, TARSKI:def_4; ::_thesis: verum
end;
hence  R is Cover of X by SETFAM_1:def_11; ::_thesis: verum
end;

theorem Th19: :: BORSUK_3:19
for X, Y being non empty compact TopSpace
for R being Subset-Family of X
for F being Subset-Family of [:Y,X:] st F is Cover of [:Y,X:] & F is open & R =  {  Q where Q is open Subset of X : ex FQ being Subset-Family of [:Y,X:] st
( FQ c= F & FQ is finite & [:([#] Y),Q:] c= union FQ )  }  holds
ex C being Subset-Family of X st
( C c= R & C is finite & C is Cover of X )
proof
let X, Y be non empty compact TopSpace; ::_thesis: for R being Subset-Family of X
for F being Subset-Family of [:Y,X:] st F is Cover of [:Y,X:] & F is open & R =  {  Q where Q is open Subset of X : ex FQ being Subset-Family of [:Y,X:] st
( FQ c= F & FQ is finite & [:([#] Y),Q:] c= union FQ )  }  holds
ex C being Subset-Family of X st
( C c= R & C is finite & C is Cover of X )
let R be Subset-Family of X; ::_thesis: for F being Subset-Family of [:Y,X:] st F is Cover of [:Y,X:] & F is open & R =  {  Q where Q is open Subset of X : ex FQ being Subset-Family of [:Y,X:] st
( FQ c= F & FQ is finite & [:([#] Y),Q:] c= union FQ )  }  holds
ex C being Subset-Family of X st
( C c= R & C is finite & C is Cover of X )
let F be Subset-Family of [:Y,X:]; ::_thesis: ( F is Cover of [:Y,X:] & F is open & R =  {  Q where Q is open Subset of X : ex FQ being Subset-Family of [:Y,X:] st
( FQ c= F & FQ is finite & [:([#] Y),Q:] c= union FQ )  }  implies ex C being Subset-Family of X st
( C c= R & C is finite & C is Cover of X ) )
assume  ( F is Cover of [:Y,X:] & F is open & R =  {  Q where Q is open Subset of X : ex FQ being Subset-Family of [:Y,X:] st
( FQ c= F & FQ is finite & [:([#] Y),Q:] c= union FQ )  }  ) ; ::_thesis: ex C being Subset-Family of X st
( C c= R & C is finite & C is Cover of X )
then  ( R is open & R is Cover of X ) by Th18;
then  ex G being Subset-Family of X st
( G c= R & G is Cover of X & G is finite ) by COMPTS_1:def_1;
hence  ex C being Subset-Family of X st
( C c= R & C is finite & C is Cover of X ) ; ::_thesis: verum
end;

theorem Th20: :: BORSUK_3:20
for X, Y being non empty compact TopSpace
for F being Subset-Family of [:Y,X:] st F is Cover of [:Y,X:] & F is open holds
ex G being Subset-Family of [:Y,X:] st
( G c= F & G is Cover of [:Y,X:] & G is finite )
proof
let X, Y be non empty compact TopSpace; ::_thesis: for F being Subset-Family of [:Y,X:] st F is Cover of [:Y,X:] & F is open holds
ex G being Subset-Family of [:Y,X:] st
( G c= F & G is Cover of [:Y,X:] & G is finite )
let F be Subset-Family of [:Y,X:]; ::_thesis: ( F is Cover of [:Y,X:] & F is open implies ex G being Subset-Family of [:Y,X:] st
( G c= F & G is Cover of [:Y,X:] & G is finite ) )
set R =  {  Q where Q is open Subset of X : ex FQ being Subset-Family of [:Y,X:] st
( FQ c= F & FQ is finite & [:([#] Y),Q:] c= union FQ )  }  ;
  {  Q where Q is open Subset of X : ex FQ being Subset-Family of [:Y,X:] st
( FQ c= F & FQ is finite & [:([#] Y),Q:] c= union FQ )  }  c= bool the carrier of X
proof
let s be set ; :: according to TARSKI:def_3 ::_thesis: ( not s in  {  Q where Q is open Subset of X : ex FQ being Subset-Family of [:Y,X:] st
( FQ c= F & FQ is finite & [:([#] Y),Q:] c= union FQ )  }  or s in bool the carrier of X )
assume  s in  {  Q where Q is open Subset of X : ex FQ being Subset-Family of [:Y,X:] st
( FQ c= F & FQ is finite & [:([#] Y),Q:] c= union FQ )  }  ; ::_thesis: s in bool the carrier of X
then  ex Q1 being open Subset of X st
( s = Q1 & ex FQ being Subset-Family of [:Y,X:] st
( FQ c= F & FQ is finite & [:([#] Y),Q1:] c= union FQ ) ) ;
hence  s in bool the carrier of X ; ::_thesis: verum
end;
then reconsider R =  {  Q where Q is open Subset of X : ex FQ being Subset-Family of [:Y,X:] st
( FQ c= F & FQ is finite & [:([#] Y),Q:] c= union FQ )  }  as Subset-Family of X ;
reconsider R = R as Subset-Family of X ;
defpred S1[ set , set ] means  ex FQ being Subset-Family of [:Y,X:] st
( FQ c= F & FQ is finite & [:([#] Y),$1:] c= union FQ & $2 = FQ );
deffunc H1( set ) ->  set = [:([#] Y),$1:];
assume  ( F is Cover of [:Y,X:] & F is open ) ; ::_thesis: ex G being Subset-Family of [:Y,X:] st
( G c= F & G is Cover of [:Y,X:] & G is finite )
then consider C being Subset-Family of X such that
A1: C c= R and
A2: C is finite and
A3: C is Cover of X by Th19;
set CX =  {  H1(f) where f is Subset of X : f in C  }  ;
  {  H1(f) where f is Subset of X : f in C  }  c= bool the carrier of [:Y,X:]
proof
let s be set ; :: according to TARSKI:def_3 ::_thesis: ( not s in  {  H1(f) where f is Subset of X : f in C  }  or s in bool the carrier of [:Y,X:] )
assume  s in  {  H1(f) where f is Subset of X : f in C  }  ; ::_thesis: s in bool the carrier of [:Y,X:]
then consider f1 being Subset of X such that
A4: s = H1(f1) and
 f1 in C ;
 [:([#] Y),f1:] c= the carrier of [:Y,X:] ;
hence  s in bool the carrier of [:Y,X:] by A4; ::_thesis: verum
end;
then reconsider CX =  {  H1(f) where f is Subset of X : f in C  }  as Subset-Family of [:Y,X:] ;
reconsider CX = CX as Subset-Family of [:Y,X:] ;
A5: for e being set st e in C holds
ex u being set st S1[e,u]
proof
let e be set ; ::_thesis: ( e in C implies ex u being set st S1[e,u] )
assume  e in C ; ::_thesis: ex u being set st S1[e,u]
then  e in R by A1;
then  ex Q1 being open Subset of X st
( Q1 = e & ex FQ being Subset-Family of [:Y,X:] st
( FQ c= F & FQ is finite & [:([#] Y),Q1:] c= union FQ ) ) ;
hence  ex u being set st S1[e,u] ; ::_thesis: verum
end;
consider t being Function such that
A6: ( dom t = C & ( for s being set st s in C holds
S1[s,t . s] ) ) from CLASSES1:sch_1(A5);
set G = union (rng t);
A7: union (rng t) c= F
proof
let k be set ; :: according to TARSKI:def_3 ::_thesis: ( not k in union (rng t) or k in F )
assume  k in union (rng t) ; ::_thesis: k in F
then consider K being set  such that
A8: k in K and
A9: K in rng t by TARSKI:def_4;
consider x1 being set  such that
A10: ( x1 in dom t & K = t . x1 ) by A9, FUNCT_1:def_3;
 ex FQ being Subset-Family of [:Y,X:] st
( FQ c= F & FQ is finite & [:([#] Y),x1:] c= union FQ & K = FQ ) by A6, A10;
hence  k in F by A8; ::_thesis: verum
end;
 union (rng t) c= bool the carrier of [:Y,X:]
proof
let s be set ; :: according to TARSKI:def_3 ::_thesis: ( not s in union (rng t) or s in bool the carrier of [:Y,X:] )
assume  s in union (rng t) ; ::_thesis: s in bool the carrier of [:Y,X:]
then  s in F by A7;
hence  s in bool the carrier of [:Y,X:] ; ::_thesis: verum
end;
then reconsider G = union (rng t) as Subset-Family of [:Y,X:] ;
reconsider G = G as Subset-Family of [:Y,X:] ;
take  G ; ::_thesis: ( G c= F & G is Cover of [:Y,X:] & G is finite )
thus  G c= F by A7; ::_thesis: ( G is Cover of [:Y,X:] & G is finite )
 union CX = [:([#] Y),(union C):]
proof
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: [:([#] Y),(union C):] c= union CX
let g be set ; ::_thesis: ( g in union CX implies g in [:([#] Y),(union C):] )
assume  g in union CX ; ::_thesis: g in [:([#] Y),(union C):]
then consider GG being set  such that
A11: g in GG and
A12: GG in CX by TARSKI:def_4;
consider FF being Subset of X such that
A13: GG = [:([#] Y),FF:] and
A14: FF in C by A12;
consider g1, g2 being set  such that
A15: g1 in [#] Y and
A16: g2 in FF and
A17: g = [g1,g2] by A11, A13, ZFMISC_1:def_2;
 g2 in union C by A14, A16, TARSKI:def_4;
hence  g in [:([#] Y),(union C):] by A15, A17, ZFMISC_1:87; ::_thesis: verum
end;
let g be set ; :: according to TARSKI:def_3 ::_thesis: ( not g in [:([#] Y),(union C):] or g in union CX )
assume  g in [:([#] Y),(union C):] ; ::_thesis: g in union CX
then consider g1, g2 being set  such that
A18: g1 in [#] Y and
A19: g2 in union C and
A20: g = [g1,g2] by ZFMISC_1:def_2;
consider GG being set  such that
A21: g2 in GG and
A22: GG in C by A19, TARSKI:def_4;
 GG in  {  Q where Q is open Subset of X : ex FQ being Subset-Family of [:Y,X:] st
( FQ c= F & FQ is finite & [:([#] Y),Q:] c= union FQ )  }  by A1, A22;
then consider Q1 being open Subset of X such that
A23: GG = Q1 and
 ex FQ being Subset-Family of [:Y,X:] st
( FQ c= F & FQ is finite & [:([#] Y),Q1:] c= union FQ ) ;
A24: [:([#] Y),Q1:] in CX by A22, A23;
 g in [:([#] Y),Q1:] by A18, A20, A21, A23, ZFMISC_1:87;
hence  g in union CX by A24, TARSKI:def_4; ::_thesis: verum
end;
then A25: union CX = [:([#] Y),([#] X):] by A3, SETFAM_1:45
.= [#] [:Y,X:] by BORSUK_1:def_2 ;
 [#] [:Y,X:] c= union (union (rng t))
proof
let d be set ; :: according to TARSKI:def_3 ::_thesis: ( not d in [#] [:Y,X:] or d in union (union (rng t)) )
assume  d in [#] [:Y,X:] ; ::_thesis: d in union (union (rng t))
then consider CC being set  such that
A26: d in CC and
A27: CC in CX by A25, TARSKI:def_4;
consider Cc being Subset of X such that
A28: CC = [:([#] Y),Cc:] and
A29: Cc in C by A27;
 Cc in R by A1, A29;
then consider Qq being open Subset of X such that
A30: Cc = Qq and
 ex FQ being Subset-Family of [:Y,X:] st
( FQ c= F & FQ is finite & [:([#] Y),Qq:] c= union FQ ) ;
consider FQ1 being Subset-Family of [:Y,X:] such that
 FQ1 c= F and
 FQ1 is finite and
A31: [:([#] Y),Qq:] c= union FQ1 and
A32: t . Qq = FQ1 by A6, A29, A30;
consider DC being set  such that
A33: d in DC and
A34: DC in FQ1 by A26, A28, A30, A31, TARSKI:def_4;
 FQ1 in rng t by A6, A29, A30, A32, FUNCT_1:def_3;
then  DC in union (rng t) by A34, TARSKI:def_4;
hence  d in union (union (rng t)) by A33, TARSKI:def_4; ::_thesis: verum
end;
hence  G is Cover of [:Y,X:] by SETFAM_1:def_11; ::_thesis: G is finite
A35: for X1 being set st X1 in rng t holds
X1 is finite
proof
let X1 be set ; ::_thesis: ( X1 in rng t implies X1 is finite )
assume  X1 in rng t ; ::_thesis: X1 is finite
then consider x1 being set  such that
A36: x1 in dom t and
A37: X1 = t . x1 by FUNCT_1:def_3;
 ex FQ being Subset-Family of [:Y,X:] st
( FQ c= F & FQ is finite & [:([#] Y),x1:] c= union FQ & t . x1 = FQ ) by A6, A36;
hence  X1 is finite by A37; ::_thesis: verum
end;
 rng t is finite by A2, A6, FINSET_1:8;
hence  G is finite by A35, FINSET_1:7; ::_thesis: verum
end;

Lm5:  for T1, T2 being non empty compact TopSpace holds [:T1,T2:] is compact
proof
let T1, T2 be non empty compact TopSpace; ::_thesis: [:T1,T2:] is compact
set T = [:T1,T2:];
let F be Subset-Family of [:T1,T2:]; :: according to COMPTS_1:def_1 ::_thesis: ( not F is Cover of the carrier of [:T1,T2:] or not F is open or ex b1 being Element of bool (bool the carrier of [:T1,T2:]) st
( b1 c= F & b1 is Cover of the carrier of [:T1,T2:] & b1 is finite ) )
assume  ( F is Cover of [:T1,T2:] & F is open ) ; ::_thesis: ex b1 being Element of bool (bool the carrier of [:T1,T2:]) st
( b1 c= F & b1 is Cover of the carrier of [:T1,T2:] & b1 is finite )
hence  ex b1 being Element of bool (bool the carrier of [:T1,T2:]) st
( b1 c= F & b1 is Cover of the carrier of [:T1,T2:] & b1 is finite ) by Th20; ::_thesis: verum
end;

registration
let T1, T2 be compact TopSpace;
cluster[:T1,T2:] ->  compact ;
coherence
 [:T1,T2:] is compact
proof
percases ( ( not T1 is empty & not T2 is empty ) or ( T1 is empty & T2 is empty ) or ( T1 is empty & not T2 is empty ) or ( not T1 is empty & T2 is empty ) ) ;
suppose ( not T1 is empty & not T2 is empty ) ; ::_thesis: [:T1,T2:] is compact
hence  [:T1,T2:] is compact by Lm5; ::_thesis: verum
end;
suppose ( T1 is empty & T2 is empty ) ; ::_thesis: [:T1,T2:] is compact
hence  [:T1,T2:] is compact ; ::_thesis: verum
end;
suppose ( T1 is empty & not T2 is empty ) ; ::_thesis: [:T1,T2:] is compact
hence  [:T1,T2:] is compact ; ::_thesis: verum
end;
suppose ( not T1 is empty & T2 is empty ) ; ::_thesis: [:T1,T2:] is compact
hence  [:T1,T2:] is compact ; ::_thesis: verum
end;
end;
end;
end;

Lm6:  for X, Y being TopSpace
for XV being SubSpace of X holds [:XV,Y:] is SubSpace of [:X,Y:]
proof
let X, Y be TopSpace; ::_thesis: for XV being SubSpace of X holds [:XV,Y:] is SubSpace of [:X,Y:]
let XV be SubSpace of X; ::_thesis: [:XV,Y:] is SubSpace of [:X,Y:]
set S = [:XV,Y:];
set T = [:X,Y:];
A1: the carrier of [:XV,Y:] = [: the carrier of XV, the carrier of Y:] by BORSUK_1:def_2;
A2: ( the carrier of [:X,Y:] = [: the carrier of X, the carrier of Y:] & the carrier of XV c= the carrier of X ) by BORSUK_1:1, BORSUK_1:def_2;
A3: for P being Subset of [:XV,Y:] holds
( P in the topology of [:XV,Y:] iff ex Q being Subset of [:X,Y:] st
( Q in the topology of [:X,Y:] & P = Q /\ ([#] [:XV,Y:]) ) )
proof
reconsider oS = [#] [:XV,Y:] as Subset of [:X,Y:] by A1, A2, ZFMISC_1:96;
let P be Subset of [:XV,Y:]; ::_thesis: ( P in the topology of [:XV,Y:] iff ex Q being Subset of [:X,Y:] st
( Q in the topology of [:X,Y:] & P = Q /\ ([#] [:XV,Y:]) ) )
reconsider P9 = P as Subset of [:XV,Y:] ;
hereby  ::_thesis: ( ex Q being Subset of [:X,Y:] st
( Q in the topology of [:X,Y:] & P = Q /\ ([#] [:XV,Y:]) ) implies P in the topology of [:XV,Y:] )
assume  P in the topology of [:XV,Y:] ; ::_thesis: ex Q being Subset of [:X,Y:] st
( Q in the topology of [:X,Y:] & P = Q /\ ([#] [:XV,Y:]) )
then  P9 is open by PRE_TOPC:def_2;
then consider A being Subset-Family of [:XV,Y:] such that
A4: P9 = union A and
A5: for e being set st e in A holds
ex X1 being Subset of XV ex Y1 being Subset of Y st
( e = [:X1,Y1:] & X1 is open & Y1 is open ) by BORSUK_1:5;
set AA =  {  [:X1,Y2:] where X1 is Subset of X, Y2 is Subset of Y : ex Y1 being Subset of XV st
( Y1 = X1 /\ ([#] XV) & X1 is open & Y2 is open & [:Y1,Y2:] in A )  }  ;
  {  [:X1,Y2:] where X1 is Subset of X, Y2 is Subset of Y : ex Y1 being Subset of XV st
( Y1 = X1 /\ ([#] XV) & X1 is open & Y2 is open & [:Y1,Y2:] in A )  }  c= bool the carrier of [:X,Y:]
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in  {  [:X1,Y2:] where X1 is Subset of X, Y2 is Subset of Y : ex Y1 being Subset of XV st
( Y1 = X1 /\ ([#] XV) & X1 is open & Y2 is open & [:Y1,Y2:] in A )  }  or a in bool the carrier of [:X,Y:] )
assume  a in  {  [:X1,Y2:] where X1 is Subset of X, Y2 is Subset of Y : ex Y1 being Subset of XV st
( Y1 = X1 /\ ([#] XV) & X1 is open & Y2 is open & [:Y1,Y2:] in A )  }  ; ::_thesis: a in bool the carrier of [:X,Y:]
then  ex Xx1 being Subset of X ex Yy2 being Subset of Y st
( a = [:Xx1,Yy2:] & ex Y1 being Subset of XV st
( Y1 = Xx1 /\ ([#] XV) & Xx1 is open & Yy2 is open & [:Y1,Yy2:] in A ) ) ;
hence  a in bool the carrier of [:X,Y:] ; ::_thesis: verum
end;
then reconsider AA =  {  [:X1,Y2:] where X1 is Subset of X, Y2 is Subset of Y : ex Y1 being Subset of XV st
( Y1 = X1 /\ ([#] XV) & X1 is open & Y2 is open & [:Y1,Y2:] in A )  }  as Subset-Family of [:X,Y:] ;
reconsider AA = AA as Subset-Family of [:X,Y:] ;
A6: P c= (union AA) /\ ([#] [:XV,Y:])
proof
let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in P or p in (union AA) /\ ([#] [:XV,Y:]) )
assume  p in P ; ::_thesis: p in (union AA) /\ ([#] [:XV,Y:])
then consider A1 being set  such that
A7: p in A1 and
A8: A1 in A by A4, TARSKI:def_4;
reconsider A1 = A1 as Subset of [:XV,Y:] by A8;
consider X2 being Subset of XV, Y2 being Subset of Y such that
A9: A1 = [:X2,Y2:] and
A10: X2 is open and
A11: Y2 is open by A5, A8;
 X2 in the topology of XV by A10, PRE_TOPC:def_2;
then consider Q1 being Subset of X such that
A12: Q1 in the topology of X and
A13: X2 = Q1 /\ ([#] XV) by PRE_TOPC:def_4;
consider p1, p2 being set  such that
A14: p1 in X2 and
A15: ( p2 in Y2 & p = [p1,p2] ) by A7, A9, ZFMISC_1:def_2;
reconsider Q1 = Q1 as Subset of X ;
set EX = [:Q1,Y2:];
 p1 in Q1 by A14, A13, XBOOLE_0:def_4;
then A16: p in [:Q1,Y2:] by A15, ZFMISC_1:87;
 Q1 is open by A12, PRE_TOPC:def_2;
then  [:Q1,Y2:] in  {  [:Xx1,Yy2:] where Xx1 is Subset of X, Yy2 is Subset of Y : ex Z1 being Subset of XV st
( Z1 = Xx1 /\ ([#] XV) & Xx1 is open & Yy2 is open & [:Z1,Yy2:] in A )  }  by A8, A9, A11, A13;
then  p in union AA by A16, TARSKI:def_4;
hence  p in (union AA) /\ ([#] [:XV,Y:]) by A7, A8, XBOOLE_0:def_4; ::_thesis: verum
end;
 AA c= the topology of [:X,Y:]
proof
let t be set ; :: according to TARSKI:def_3 ::_thesis: ( not t in AA or t in the topology of [:X,Y:] )
set A9 = {t};
assume  t in AA ; ::_thesis: t in the topology of [:X,Y:]
then consider Xx1 being Subset of X, Yy2 being Subset of Y such that
A17: t = [:Xx1,Yy2:] and
A18: ex Y1 being Subset of XV st
( Y1 = Xx1 /\ ([#] XV) & Xx1 is open & Yy2 is open & [:Y1,Yy2:] in A ) ;
 {t} c= bool the carrier of [:X,Y:]
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in {t} or a in bool the carrier of [:X,Y:] )
assume  a in {t} ; ::_thesis: a in bool the carrier of [:X,Y:]
then  a = t by TARSKI:def_1;
hence  a in bool the carrier of [:X,Y:] by A17; ::_thesis: verum
end;
then reconsider A9 = {t} as Subset-Family of [:X,Y:] ;
A19: A9 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 x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A9 or 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 )  }  )
assume  x in A9 ; ::_thesis: 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 )  }
then A20: x = [:Xx1,Yy2:] by A17, TARSKI:def_1;
 ( Xx1 in the topology of X & Yy2 in the topology of Y ) by A18, PRE_TOPC:def_2;
hence  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 A20; ::_thesis: verum
end;
 t = union A9 by ZFMISC_1:25;
then  t in  {  (union As) where As is Subset-Family of [:X,Y:] : As 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 A19;
hence  t in the topology of [:X,Y:] by BORSUK_1:def_2; ::_thesis: verum
end;
then A21: union AA in the topology of [:X,Y:] by PRE_TOPC:def_1;
 (union AA) /\ ([#] [:XV,Y:]) c= P
proof
let h be set ; :: according to TARSKI:def_3 ::_thesis: ( not h in (union AA) /\ ([#] [:XV,Y:]) or h in P )
assume A22: h in (union AA) /\ ([#] [:XV,Y:]) ; ::_thesis: h in P
then  h in union AA by XBOOLE_0:def_4;
then consider A2 being set  such that
A23: h in A2 and
A24: A2 in AA by TARSKI:def_4;
consider Xx1 being Subset of X, Yy2 being Subset of Y such that
A25: A2 = [:Xx1,Yy2:] and
A26: ex Y1 being Subset of XV st
( Y1 = Xx1 /\ ([#] XV) & Xx1 is open & Yy2 is open & [:Y1,Yy2:] in A ) by A24;
consider Yy1 being Subset of XV such that
A27: Yy1 = Xx1 /\ ([#] XV) and
 Xx1 is open and
 Yy2 is open and
A28: [:Yy1,Yy2:] in A by A26;
consider p1, p2 being set  such that
A29: p1 in Xx1 and
A30: p2 in Yy2 and
A31: h = [p1,p2] by A23, A25, ZFMISC_1:def_2;
 p1 in the carrier of XV by A1, A22, A31, ZFMISC_1:87;
then  p1 in Xx1 /\ ([#] XV) by A29, XBOOLE_0:def_4;
then  h in [:Yy1,Yy2:] by A30, A31, A27, ZFMISC_1:87;
hence  h in P by A4, A28, TARSKI:def_4; ::_thesis: verum
end;
then  P = (union AA) /\ ([#] [:XV,Y:]) by A6, XBOOLE_0:def_10;
hence  ex Q being Subset of [:X,Y:] st
( Q in the topology of [:X,Y:] & P = Q /\ ([#] [:XV,Y:]) ) by A21; ::_thesis: verum
end;
given Q being Subset of [:X,Y:] such that A32: Q in the topology of [:X,Y:] and
A33: P = Q /\ ([#] [:XV,Y:]) ; ::_thesis: P in the topology of [:XV,Y:]
reconsider Q9 = Q as Subset of [:X,Y:] ;
 Q9 is open by A32, PRE_TOPC:def_2;
then consider A being Subset-Family of [:X,Y:] such that
A34: Q9 = union A and
A35: 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 BORSUK_1:5;
reconsider A = A as Subset-Family of [:X,Y:] ;
reconsider AA = A | oS as Subset-Family of ([:X,Y:] | oS) ;
reconsider AA = AA as Subset-Family of [:XV,Y:] by PRE_TOPC:8;
reconsider AA = AA as Subset-Family of [:XV,Y:] ;
A36: for e being set st e in AA holds
ex X1 being Subset of XV ex Y1 being Subset of Y st
( e = [:X1,Y1:] & X1 is open & Y1 is open )
proof
let e be set ; ::_thesis: ( e in AA implies ex X1 being Subset of XV ex Y1 being Subset of Y st
( e = [:X1,Y1:] & X1 is open & Y1 is open ) )
assume A37: e in AA ; ::_thesis: ex X1 being Subset of XV ex Y1 being Subset of Y st
( e = [:X1,Y1:] & X1 is open & Y1 is open )
then reconsider e9 = e as Subset of ([:X,Y:] | oS) ;
consider R being Subset of [:X,Y:] such that
A38: R in A and
A39: R /\ oS = e9 by A37, TOPS_2:def_3;
consider X1 being Subset of X, Y1 being Subset of Y such that
A40: R = [:X1,Y1:] and
A41: X1 is open and
A42: Y1 is open by A35, A38;
reconsider D2 = X1 /\ ([#] XV) as Subset of XV ;
 X1 in the topology of X by A41, PRE_TOPC:def_2;
then  D2 in the topology of XV by PRE_TOPC:def_4;
then A43: D2 is open by PRE_TOPC:def_2;
 [#] [:XV,Y:] = [:([#] XV),([#] Y):] by BORSUK_1:def_2;
then  e9 = [:(X1 /\ ([#] XV)),(Y1 /\ ([#] Y)):] by A39, A40, ZFMISC_1:100;
hence  ex X1 being Subset of XV ex Y1 being Subset of Y st
( e = [:X1,Y1:] & X1 is open & Y1 is open ) by A42, A43; ::_thesis: verum
end;
A44: (union A) /\ oS c= union AA
proof
let s be set ; :: according to TARSKI:def_3 ::_thesis: ( not s in (union A) /\ oS or s in union AA )
assume A45: s in (union A) /\ oS ; ::_thesis: s in union AA
then  s in union A by XBOOLE_0:def_4;
then consider A1 being set  such that
A46: s in A1 and
A47: A1 in A by TARSKI:def_4;
 s in oS by A45, XBOOLE_0:def_4;
then A48: s in A1 /\ oS by A46, XBOOLE_0:def_4;
reconsider A1 = A1 as Subset of [:X,Y:] by A47;
 A1 /\ oS in AA by A47, TOPS_2:31;
hence  s in union AA by A48, TARSKI:def_4; ::_thesis: verum
end;
 union AA c= union A by TOPS_2:34;
then  union AA c= (union A) /\ oS by XBOOLE_1:19;
then  P = union AA by A33, A34, A44, XBOOLE_0:def_10;
then  P9 is open by A36, BORSUK_1:5;
hence  P in the topology of [:XV,Y:] by PRE_TOPC:def_2; ::_thesis: verum
end;
 [#] [:XV,Y:] c= [#] [:X,Y:] by A1, A2, ZFMISC_1:96;
hence  [:XV,Y:] is SubSpace of [:X,Y:] by A3, PRE_TOPC:def_4; ::_thesis: verum
end;

theorem Th21: :: BORSUK_3:21
for X, Y being TopSpace
for XV being SubSpace of X
for YV being SubSpace of Y holds [:XV,YV:] is SubSpace of [:X,Y:]
proof
let X, Y be TopSpace; ::_thesis: for XV being SubSpace of X
for YV being SubSpace of Y holds [:XV,YV:] is SubSpace of [:X,Y:]
let XV be SubSpace of X; ::_thesis: for YV being SubSpace of Y holds [:XV,YV:] is SubSpace of [:X,Y:]
let YV be SubSpace of Y; ::_thesis: [:XV,YV:] is SubSpace of [:X,Y:]
 ( [:XV,Y:] is SubSpace of [:X,Y:] & [:XV,YV:] is SubSpace of [:XV,Y:] ) by Lm6, Th15;
hence  [:XV,YV:] is SubSpace of [:X,Y:] by TSEP_1:7; ::_thesis: verum
end;

theorem Th22: :: BORSUK_3:22
for X, Y being TopSpace
for Z being Subset of [:Y,X:]
for V being Subset of X
for W being Subset of Y st Z = [:W,V:] holds
TopStruct(# the carrier of [:(Y | W),(X | V):], the topology of [:(Y | W),(X | V):] #) = TopStruct(# the carrier of ([:Y,X:] | Z), the topology of ([:Y,X:] | Z) #)
proof
let X, Y be TopSpace; ::_thesis: for Z being Subset of [:Y,X:]
for V being Subset of X
for W being Subset of Y st Z = [:W,V:] holds
TopStruct(# the carrier of [:(Y | W),(X | V):], the topology of [:(Y | W),(X | V):] #) = TopStruct(# the carrier of ([:Y,X:] | Z), the topology of ([:Y,X:] | Z) #)
let Z be Subset of [:Y,X:]; ::_thesis: for V being Subset of X
for W being Subset of Y st Z = [:W,V:] holds
TopStruct(# the carrier of [:(Y | W),(X | V):], the topology of [:(Y | W),(X | V):] #) = TopStruct(# the carrier of ([:Y,X:] | Z), the topology of ([:Y,X:] | Z) #)
let V be Subset of X; ::_thesis: for W being Subset of Y st Z = [:W,V:] holds
TopStruct(# the carrier of [:(Y | W),(X | V):], the topology of [:(Y | W),(X | V):] #) = TopStruct(# the carrier of ([:Y,X:] | Z), the topology of ([:Y,X:] | Z) #)
let W be Subset of Y; ::_thesis: ( Z = [:W,V:] implies TopStruct(# the carrier of [:(Y | W),(X | V):], the topology of [:(Y | W),(X | V):] #) = TopStruct(# the carrier of ([:Y,X:] | Z), the topology of ([:Y,X:] | Z) #) )
reconsider A = [:(Y | W),(X | V):] as SubSpace of [:Y,X:] by Th21;
assume A1: Z = [:W,V:] ; ::_thesis: TopStruct(# the carrier of [:(Y | W),(X | V):], the topology of [:(Y | W),(X | V):] #) = TopStruct(# the carrier of ([:Y,X:] | Z), the topology of ([:Y,X:] | Z) #)
the carrier of A = [: the carrier of (Y | W), the carrier of (X | V):] by BORSUK_1:def_2
.= [: the carrier of (Y | W),V:] by PRE_TOPC:8
.= Z by A1, PRE_TOPC:8
.= the carrier of ([:Y,X:] | Z) by PRE_TOPC:8 ;
then  ( A is SubSpace of [:Y,X:] | Z & [:Y,X:] | Z is SubSpace of A ) by TOPMETR:3;
hence  TopStruct(# the carrier of [:(Y | W),(X | V):], the topology of [:(Y | W),(X | V):] #) = TopStruct(# the carrier of ([:Y,X:] | Z), the topology of ([:Y,X:] | Z) #) by TSEP_1:6; ::_thesis: verum
end;

registration
let T be TopSpace;
cluster empty for Element of bool the carrier of T;
existence
 ex b1 being Subset of T st b1 is empty
proof
take  {} T ; ::_thesis: {} T is empty
thus  {} T is empty ; ::_thesis: verum
end;
end;

registration
let T be TopSpace;
let P be compact Subset of T;
clusterT | P ->  compact ;
coherence
 T | P is compact
proof
percases ( not P is empty or P is empty ) ;
suppose not P is empty ; ::_thesis: T | P is compact
hence  T | P is compact by COMPTS_1:3; ::_thesis: verum
end;
suppose P is empty ; ::_thesis: T | P is compact
hence  T | P is compact ; ::_thesis: verum
end;
end;
end;
end;

theorem :: BORSUK_3:23
for T1, T2 being TopSpace
for S1 being Subset of T1
for S2 being Subset of T2 st S1 is compact & S2 is compact holds
[:S1,S2:] is compact Subset of [:T1,T2:]
proof
let T1, T2 be TopSpace; ::_thesis: for S1 being Subset of T1
for S2 being Subset of T2 st S1 is compact & S2 is compact holds
[:S1,S2:] is compact Subset of [:T1,T2:]
let S1 be Subset of T1; ::_thesis: for S2 being Subset of T2 st S1 is compact & S2 is compact holds
[:S1,S2:] is compact Subset of [:T1,T2:]
let S2 be Subset of T2; ::_thesis: ( S1 is compact & S2 is compact implies [:S1,S2:] is compact Subset of [:T1,T2:] )
assume that
A1: S1 is compact and
A2: S2 is compact ; ::_thesis: [:S1,S2:] is compact Subset of [:T1,T2:]
percases ( ( not S1 is empty & not S2 is empty ) or ( S1 is empty & not S2 is empty ) or ( not S1 is empty & S2 is empty ) or ( S1 is empty & S2 is empty ) ) ;
supposeA3: ( not S1 is empty & not S2 is empty ) ; ::_thesis: [:S1,S2:] is compact Subset of [:T1,T2:]
then  ( ex x being set st x in S1 & ex y being set st y in S2 ) by XBOOLE_0:def_1;
then reconsider T1 = T1, T2 = T2 as non empty TopSpace ;
reconsider S2 = S2 as non empty compact Subset of T2 by A2, A3;
reconsider S1 = S1 as non empty compact Subset of T1 by A1, A3;
reconsider X = [:S1,S2:] as Subset of [:T1,T2:] ;
 TopStruct(# the carrier of [:(T1 | S1),(T2 | S2):], the topology of [:(T1 | S1),(T2 | S2):] #) = TopStruct(# the carrier of ([:T1,T2:] | X), the topology of ([:T1,T2:] | X) #) by Th22;
hence  [:S1,S2:] is compact Subset of [:T1,T2:] by COMPTS_1:3; ::_thesis: verum
end;
suppose ( S1 is empty & not S2 is empty ) ; ::_thesis: [:S1,S2:] is compact Subset of [:T1,T2:]
then reconsider S1 = S1 as empty Subset of T1 ;
 [:S1,S2:] = {} [:T1,T2:] ;
hence  [:S1,S2:] is compact Subset of [:T1,T2:] ; ::_thesis: verum
end;
suppose ( not S1 is empty & S2 is empty ) ; ::_thesis: [:S1,S2:] is compact Subset of [:T1,T2:]
then reconsider S2 = S2 as empty Subset of T2 ;
 [:S1,S2:] = {} [:T1,T2:] ;
hence  [:S1,S2:] is compact Subset of [:T1,T2:] ; ::_thesis: verum
end;
suppose ( S1 is empty & S2 is empty ) ; ::_thesis: [:S1,S2:] is compact Subset of [:T1,T2:]
then reconsider S2 = S2 as empty Subset of T2 ;
 [:S1,S2:] = {} [:T1,T2:] ;
hence  [:S1,S2:] is compact Subset of [:T1,T2:] ; ::_thesis: verum
end;
end;
end;