:: BORSUK_3 semantic presentation

theorem E1: :: BORSUK_3:1
for b1, b2 being TopSpace holds [#] [:b1,b2:] = [:([#] b1),([#] b2):]
proof
let c1, c2 be TopSpace;
E2: ( the carrier of c1 = [#] c1 & the carrier of c2 = [#] c2 ) by PRE_TOPC:12;
[#] [:c1,c2:] = the carrier of [:c1,c2:] by PRE_TOPC:12
.= [:([#] c1),([#] c2):] by E2, BORSUK_1:def 5 ;
hence [#] [:c1,c2:] = [:([#] c1),([#] c2):] ;
end;

registration
let c1 be set ;
let c2 be empty set ;
cluster [:a1,a2:] -> empty ;
coherence
[:c1,c2:] is empty by ZFMISC_1:113;
end;

registration
let c1 be empty set ;
let c2 be set ;
cluster [:a1,a2:] -> empty ;
coherence
[:c1,c2:] is empty by ZFMISC_1:113;
end;

theorem E2: :: BORSUK_3:2
for b1, b2 being non empty TopSpace
for b3 being Point of b1 holds
b2 --> b3 is continuous Function of b2,(b1 | {b3})
proof
let c1, c2 be non empty TopSpace;
let c3 be Point of c1;
set c4 = {c3};
set c5 = c2 --> c3;
E3: c2 --> c3 = the carrier of c2 --> c3 by BORSUK_1:def 3;
E4: c3 in {c3} by TARSKI:def 1;
the carrier of (c1 | {c3}) = {c3} by JORDAN1:1;
then reconsider c6 = c2 --> c3 as Function of c2,(c1 | {c3}) by E3, E4, FUNCOP_1:57;
c6 is continuous by TOPMETR:9;
hence c2 --> c3 is continuous Function of c2,(c1 | {c3}) ;
end;

registration
let c1 be non empty TopStruct ;
cluster id a1 -> being_homeomorphism ;
coherence
id c1 is being_homeomorphism by TOPGRP_1:20;
end;

E3: for b1 being non empty TopStruct holds b1,b1 are_homeomorphic
proof
let c1 be non empty TopStruct ;
take id c1 ; :: uses T_0TOPSP:def 1
thus id c1 is being_homeomorphism ;
end;

E4: for b1, b2 being non empty TopStruct holds
( b1,b2 are_homeomorphic implies b2,b1 are_homeomorphic )
proof
let c1, c2 be non empty TopStruct ;
assume c1,c2 are_homeomorphic ;
then consider c3 being Function of c1,c2 such that
E5: c3 is is_homeomorphism by T_0TOPSP:def 1;
c3 " is is_homeomorphism by E5, TOPS_2:70;
hence c2,c1 are_homeomorphic by T_0TOPSP:def 1;
end;

definition
let c1, c2 be non empty TopStruct ;
redefine pred are_homeomorphic as a1,a2 are_homeomorphic ;
reflexivity
for b1 being non empty TopStruct holds b1,b1 are_homeomorphic by E3;
symmetry
for b1, b2 being non empty TopStruct holds
( b1,b2 are_homeomorphic implies b2,b1 are_homeomorphic ) by E4;
end;

theorem :: BORSUK_3:3
for b1, b2, b3 being non empty TopSpace holds
( ( b1,b2 are_homeomorphic & b2,b3 are_homeomorphic ) implies ( b1,b3 are_homeomorphic ) )
proof
let c1, c2, c3 be non empty TopSpace;
assume E5: ( c1,c2 are_homeomorphic & c2,c3 are_homeomorphic ) ;
then consider c4 being Function of c1,c2 such that
E6: c4 is is_homeomorphism by T_0TOPSP:def 1;
consider c5 being Function of c2,c3 such that
E7: c5 is is_homeomorphism by E5, T_0TOPSP:def 1;
c5 * c4 is is_homeomorphism by E6, E7, TOPS_2:71;
hence c1,c3 are_homeomorphic by T_0TOPSP:def 1;
end;

registration
let c1 be TopStruct ;
let c2 be empty Subset of c1;
cluster a1 | a2 -> empty ;
coherence
c1 | c2 is empty
proof
the carrier of (c1 | c2) = c2 by JORDAN1:1;
hence c1 | c2 is empty by STRUCT_0:def 1;
end;
end;

registration
cluster empty strict TopStruct ;
existence
ex b1 being TopSpace st
( b1 is strict & b1 is empty )
proof
consider c1 being TopSpace;
take c1 | ({} c1) ;
thus ( c1 | ({} c1) is strict & c1 | ({} c1) is empty ) ;
end;
end;

theorem E5: :: BORSUK_3:4
for b1 being TopSpace
for b2 being empty TopSpace holds
( [:b1,b2:] is empty & [:b2,b1:] is empty )
proof
let c1 be TopSpace;
let c2 be empty TopSpace;
( the carrier of [:c1,c2:] = [:the carrier of c1,the carrier of c2:] & the carrier of [:c2,c1:] = [:the carrier of c2,the carrier of c1:] ) by BORSUK_1:def 5;
hence ( [:c1,c2:] is empty & [:c2,c1:] is empty ) by STRUCT_0:def 1;
end;

theorem E6: :: BORSUK_3:5
for b1 being empty TopSpace holds b1 is compact
proof
let c1 be empty TopSpace;
{} c1 is compact by COMPTS_1:9;
then [#] c1 is compact ;
hence c1 is compact by COMPTS_1:10;
end;

registration
cluster empty -> compact TopStruct ;
coherence
for b1 being TopSpace holds
( b1 is empty implies b1 is compact ) by E6;
end;

registration
let c1 be TopSpace;
let c2 be empty TopSpace;
cluster [:a1,a2:] -> empty compact ;
coherence
[:c1,c2:] is empty by E5;
end;

theorem E7: :: BORSUK_3:6
for b1, b2 being non empty TopSpace
for b3 being Point of b1
for b4 being Function of [:b2,(b1 | {b3}):],b2 holds
( b4 = pr1 the carrier of b2,{b3} implies b4 is one-to-one )
proof
let c1, c2 be non empty TopSpace;
let c3 be Point of c1;
let c4 be Function of [:c2,(c1 | {c3}):],c2;
set c5 = {c3};
assume E8: c4 = pr1 the carrier of c2,{c3} ;
then E9: dom c4 = [:the carrier of c2,{c3}:] by FUNCT_3:def 5;
let c6, c7 be set ; :: uses FUNCT_1:def 8
assume that E10: ( c6 in dom c4 & c7 in dom c4 )
and E11: c4 . c6 = c4 . c7 ;
consider c8, c9 being set such that
E12: ( c8 in the carrier of c2 & c9 in {c3} & c6 = [c8,c9] ) by E9, E10, ZFMISC_1:def 2;
consider c10, c11 being set such that
E13: ( c10 in the carrier of c2 & c11 in {c3} & c7 = [c10,c11] ) by E9, E10, ZFMISC_1:def 2;
E14: c9 = c3 by E12, TARSKI:def 1
.= c11 by E13, TARSKI:def 1 ;
c8 = c4 . [c10,c11] by E8, E11, E12, E13, FUNCT_3:def 5
.= c10 by E8, E13, FUNCT_3:def 5 ;
hence c6 = c7 by E12, E13, E14;
end;

theorem E8: :: BORSUK_3:7
for b1, b2 being non empty TopSpace
for b3 being Point of b1
for b4 being Function of [:(b1 | {b3}),b2:],b2 holds
( b4 = pr2 {b3},the carrier of b2 implies b4 is one-to-one )
proof
let c1, c2 be non empty TopSpace;
let c3 be Point of c1;
let c4 be Function of [:(c1 | {c3}),c2:],c2;
set c5 = {c3};
assume E9: c4 = pr2 {c3},the carrier of c2 ;
then E10: dom c4 = [:{c3},the carrier of c2:] by FUNCT_3:def 6;
let c6, c7 be set ; :: uses FUNCT_1:def 8
assume that E11: ( c6 in dom c4 & c7 in dom c4 )
and E12: c4 . c6 = c4 . c7 ;
consider c8, c9 being set such that
E13: ( c8 in {c3} & c9 in the carrier of c2 & c6 = [c8,c9] ) by E10, E11, ZFMISC_1:def 2;
consider c10, c11 being set such that
E14: ( c10 in {c3} & c11 in the carrier of c2 & c7 = [c10,c11] ) by E10, E11, ZFMISC_1:def 2;
E15: c8 = c3 by E13, TARSKI:def 1
.= c10 by E14, TARSKI:def 1 ;
c9 = c4 . [c10,c11] by E9, E12, E13, E14, FUNCT_3:def 6
.= c11 by E9, E14, FUNCT_3:def 6 ;
hence c6 = c7 by E13, E14, E15;
end;

theorem E9: :: BORSUK_3:8
for b1, b2 being non empty TopSpace
for b3 being Point of b1
for b4 being Function of [:b2,(b1 | {b3}):],b2 holds
( b4 = pr1 the carrier of b2,{b3} implies b4 " = <:(id b2),(b2 --> b3):> )
proof
let c1, c2 be non empty TopSpace;
let c3 be Point of c1;
let c4 be Function of [:c2,(c1 | {c3}):],c2;
set c5 = {c3};
assume E10: c4 = pr1 the carrier of c2,{c3} ;
then E11: rng c4 = the carrier of c2 by FUNCT_3:60
.= [#] c2 by PRE_TOPC:12 ;
E12: c4 is one-to-one by E10, E7;
reconsider c6 = {c3} as non empty Subset of c1 ;
reconsider c7 = c2 --> c3 as continuous Function of c2,(c1 | c6) by E2;
set c8 = id c2;
reconsider c9 = <:(id c2),c7:> as continuous Function of c2,[:c2,(c1 | c6):] by YELLOW12:41;
E13: rng c9 c= [:(rng (id c2)),(rng c7):] by FUNCT_3:71;
rng c7 c= the carrier of (c1 | c6) by RELSET_1:12;
then E14: rng c7 c= c6 by JORDAN1:1;
rng (id c2) c= the carrier of c2 by RELSET_1:12;
then [:(rng (id c2)),(rng c7):] c= [:the carrier of c2,c6:] by E14, ZFMISC_1:119;
then E15: rng c9 c= [:the carrier of c2,c6:] by E13, XBOOLE_1:1;
[:the carrier of c2,c6:] c= rng c9
proof
let c10 be set ; :: uses TARSKI:def 3
assume c10 in [:the carrier of c2,c6:] ;
then consider c11, c12 being set such that
E16: ( c11 in the carrier of c2 & c12 in {c3} & c10 = [c11,c12] ) by ZFMISC_1:def 2;
E17: c10 = [c11,c3] by E16, TARSKI:def 1;
E18: c7 . c11 = (the carrier of c2 --> c3) . c11 by BORSUK_1:def 3
.= c3 by E16, FUNCOP_1:13 ;
E19: c11 in dom c9 by E16, FUNCT_2:def 1;
then c9 . c11 = [((id c2) . c11),(c7 . c11)] by FUNCT_3:def 8
.= [c11,c3] by E16, E18, GRCAT_1:11 ;
hence c10 in rng c9 by E17, E19, FUNCT_1:def 5;
end;
then E16: rng c9 = [:the carrier of c2,c6:] by E15, XBOOLE_0:def 10
.= dom c4 by E10, FUNCT_3:def 5 ;
E17: dom c7 = the carrier of c2 by FUNCT_2:def 1
.= dom (id c2) by FUNCT_2:def 1 ;
rng (id c2) c= the carrier of c2 by RELSET_1:12;
then c9 * c4 = id c2 by E10, E14, E17, FUNCT_3:72
.= id the carrier of c2 by GRCAT_1:def 11
.= id (rng c4) by E11, PRE_TOPC:12 ;
then c9 = c4 " by E12, E16, FUNCT_1:64;
hence c4 " = <:(id c2),(c2 --> c3):> by E11, E12, TOPS_2:def 4;
end;

theorem E10: :: BORSUK_3:9
for b1, b2 being non empty TopSpace
for b3 being Point of b1
for b4 being Function of [:(b1 | {b3}),b2:],b2 holds
( b4 = pr2 {b3},the carrier of b2 implies b4 " = <:(b2 --> b3),(id b2):> )
proof
let c1, c2 be non empty TopSpace;
let c3 be Point of c1;
let c4 be Function of [:(c1 | {c3}),c2:],c2;
set c5 = {c3};
assume E11: c4 = pr2 {c3},the carrier of c2 ;
then E12: rng c4 = the carrier of c2 by FUNCT_3:62
.= [#] c2 by PRE_TOPC:12 ;
E13: c4 is one-to-one by E11, E8;
reconsider c6 = {c3} as non empty Subset of c1 ;
reconsider c7 = c2 --> c3 as continuous Function of c2,(c1 | c6) by E2;
set c8 = id c2;
reconsider c9 = <:c7,(id c2):> as continuous Function of c2,[:(c1 | c6),c2:] by YELLOW12:41;
E14: rng c9 c= [:(rng c7),(rng (id c2)):] by FUNCT_3:71;
rng c7 c= the carrier of (c1 | c6) by RELSET_1:12;
then E15: rng c7 c= c6 by JORDAN1:1;
rng (id c2) c= the carrier of c2 by RELSET_1:12;
then [:(rng c7),(rng (id c2)):] c= [:{c3},the carrier of c2:] by E15, ZFMISC_1:119;
then E16: rng c9 c= [:{c3},the carrier of c2:] by E14, XBOOLE_1:1;
[:{c3},the carrier of c2:] c= rng c9
proof
let c10 be set ; :: uses TARSKI:def 3
assume c10 in [:{c3},the carrier of c2:] ;
then consider c11, c12 being set such that
E17: ( c11 in {c3} & c12 in the carrier of c2 & c10 = [c11,c12] ) by ZFMISC_1:def 2;
E18: c10 = [c3,c12] by E17, TARSKI:def 1;
E19: c7 . c12 = (the carrier of c2 --> c3) . c12 by BORSUK_1:def 3
.= c3 by E17, FUNCOP_1:13 ;
E20: c12 in dom c9 by E17, FUNCT_2:def 1;
then c9 . c12 = [(c7 . c12),((id c2) . c12)] by FUNCT_3:def 8
.= [c3,c12] by E17, E19, GRCAT_1:11 ;
hence c10 in rng c9 by E18, E20, FUNCT_1:def 5;
end;
then E17: rng c9 = [:c6,the carrier of c2:] by E16, XBOOLE_0:def 10
.= dom c4 by E11, FUNCT_3:def 6 ;
E18: dom c7 = the carrier of c2 by FUNCT_2:def 1
.= dom (id c2) by FUNCT_2:def 1 ;
rng (id c2) c= the carrier of c2 by RELSET_1:12;
then c9 * c4 = id c2 by E11, E15, E18, FUNCT_3:72
.= id the carrier of c2 by GRCAT_1:def 11
.= id (rng c4) by E12, PRE_TOPC:12 ;
then c9 = c4 " by E13, E17, FUNCT_1:64;
hence c4 " = <:(c2 --> c3),(id c2):> by E12, E13, TOPS_2:def 4;
end;

theorem :: BORSUK_3:10
for b1, b2 being non empty TopSpace
for b3 being Point of b1
for b4 being Function of [:b2,(b1 | {b3}):],b2 holds
( b4 = pr1 the carrier of b2,{b3} implies b4 is is_homeomorphism )
proof
let c1, c2 be non empty TopSpace;
let c3 be Point of c1;
let c4 be Function of [:c2,(c1 | {c3}):],c2;
set c5 = {c3};
assume E11: c4 = pr1 the carrier of c2,{c3} ;
E12: the carrier of (c1 | {c3}) = {c3} by JORDAN1:1;
thus dom c4 = the carrier of [:c2,(c1 | {c3}):] by FUNCT_2:def 1
.= [#] [:c2,(c1 | {c3}):] by PRE_TOPC:12 ; :: uses TOPS_2:def 5
thus rng c4 = the carrier of c2 by E11, FUNCT_3:60
.= [#] c2 by PRE_TOPC:12 ;
thus c4 is one-to-one by E11, E7;
thus c4 is continuous by E11, E12, YELLOW12:39;
reconsider c6 = {c3} as non empty Subset of c1 ;
reconsider c7 = c2 --> c3 as continuous Function of c2,(c1 | c6) by E2;
reconsider c8 = <:(id c2),c7:> as continuous Function of c2,[:c2,(c1 | c6):] by YELLOW12:41;
c8 = c4 " by E11, E9;
hence c4 " is continuous ;
end;

theorem E11: :: BORSUK_3:11
for b1, b2 being non empty TopSpace
for b3 being Point of b1
for b4 being Function of [:(b1 | {b3}),b2:],b2 holds
( b4 = pr2 {b3},the carrier of b2 implies b4 is is_homeomorphism )
proof
let c1, c2 be non empty TopSpace;
let c3 be Point of c1;
let c4 be Function of [:(c1 | {c3}),c2:],c2;
set c5 = {c3};
assume E12: c4 = pr2 {c3},the carrier of c2 ;
E13: the carrier of (c1 | {c3}) = {c3} by JORDAN1:1;
thus dom c4 = the carrier of [:(c1 | {c3}),c2:] by FUNCT_2:def 1
.= [#] [:(c1 | {c3}),c2:] by PRE_TOPC:12 ; :: uses TOPS_2:def 5
thus rng c4 = the carrier of c2 by E12, FUNCT_3:62
.= [#] c2 by PRE_TOPC:12 ;
thus c4 is one-to-one by E12, E8;
thus c4 is continuous by E12, E13, YELLOW12:40;
reconsider c6 = {c3} as non empty Subset of c1 ;
reconsider c7 = c2 --> c3 as continuous Function of c2,(c1 | c6) by E2;
reconsider c8 = <:c7,(id c2):> as continuous Function of c2,[:(c1 | c6),c2:] by YELLOW12:41;
c8 = c4 " by E12, E10;
hence c4 " is continuous ;
end;

theorem :: BORSUK_3:12
for b1 being non empty TopSpace
for b2 being non empty compact TopSpace
for b3 being open Subset of [:b1,b2:]
for b4 being set holds
not ( b4 in { b5 where B is Point of b1 : [:{b5},the carrier of b2:] c= b3 } & for b5 being ManySortedSet of the carrier of b2 holds
ex b6 being set st
( b6 in the carrier of b2 & for b7 being Subset of b1
for b8 being Subset of b2 holds
not ( b5 . b6 = [b7,b8] & [b4,b6] in [:b7,b8:] & b7 is open & b8 is open & [:b7,b8:] c= b3 ) ) )
proof
let c1 be non empty TopSpace;
let c2 be non empty compact TopSpace;
let c3 be open Subset of [:c1,c2:];
let c4 be set ;
assume c4 in { b1 where B is Point of c1 : [:{b1},the carrier of c2:] c= c3 } ;
then consider c5 being Point of c1 such that
E12: ( c4 = c5 & [:{c5},the carrier of c2:] c= c3 ) ;
E13: [:{c5},the carrier of c2:] c= union (Base-Appr c3) by E12, BORSUK_1:54;
E14: now
let c6 be set ;
assume E15: c6 in the carrier of c2 ;
c4 in {c5} by E12, TARSKI:def 1;
then [c4,c6] in [:{c5},the carrier of c2:] by E15, ZFMISC_1:106;
then consider c7 being set such that
E16: ( [c4,c6] in c7 & c7 in Base-Appr c3 ) by E13, TARSKI:def 4;
Base-Appr c3 = { [:b1,b2:] where B is Subset of c1, B is Subset of c2 : ( [:b1,b2:] c= c3 & b1 is open & b2 is open ) } by BORSUK_1:def 6;
then consider c8 being Subset of c1, c9 being Subset of c2 such that
E17: ( c7 = [:c8,c9:] & [:c8,c9:] c= c3 & c8 is open & c9 is open ) by E16;
thus ex b1 being Subset of c1ex b2 being Subset of c2 st
( [c4,c6] in [:b1,b2:] & [:b1,b2:] c= c3 & b1 is open & b2 is open ) by E16, E17;
end;
defpred S1[ set , set ] means ex b1 being Subset of c1ex b2 being Subset of c2 st
( a2 = [b1,b2] & [c4,a1] in [:b1,b2:] & b1 is open & b2 is open & [:b1,b2:] c= c3 );
E15: for b1 being set holds
not ( b1 in the carrier of c2 & for b2 being set holds
not S1[b1,b2] )
proof
let c6 be set ;
assume c6 in the carrier of c2 ;
then consider c7 being Subset of c1, c8 being Subset of c2 such that
E16: ( [c4,c6] in [:c7,c8:] & [:c7,c8:] c= c3 & c7 is open & c8 is open ) by E14;
ex b1 being Subset of c1ex b2 being Subset of c2 st
( [c7,c8] = [b1,b2] & [c4,c6] in [:b1,b2:] & b1 is open & b2 is open & [:b1,b2:] c= c3 ) by E16;
hence ex b1 being set st
S1[c6,b1] ;
end;
ex b1 being ManySortedSet of the carrier of c2 st
for b2 being set holds
( b2 in the carrier of c2 implies S1[b2,b1 . b2] ) from PBOOLE:sch 3(E15);
 hence ex b1 being ManySortedSet of the carrier of c2 st
for b2 being set holds
not ( b2 in the carrier of c2 & for b3 being Subset of c1
for b4 being Subset of c2 holds
not ( b1 . b2 = [b3,b4] & [c4,b2] in [:b3,b4:] & b3 is open & b4 is open & [:b3,b4:] c= c3 ) ) ;
end;

theorem E12: :: BORSUK_3:13
for b1 being non empty TopSpace
for b2 being non empty compact TopSpace
for b3 being open Subset of [:b2,b1:]
for b4 being set holds
not ( b4 in { b5 where B is Point of b1 : [:([#] b2),{b5}:] c= b3 } & for b5 being open Subset of b1 holds
not ( b4 in b5 & b5 c= { b6 where B is Point of b1 : [:([#] b2),{b6}:] c= b3 } ) )
proof
let c1 be non empty TopSpace;
let c2 be non empty compact TopSpace;
let c3 be open Subset of [:c2,c1:];
let c4 be set ;
assume c4 in { b1 where B is Point of c1 : [:([#] c2),{b1}:] c= c3 } ;
then consider c5 being Point of c1 such that
E13: ( c5 = c4 & [:([#] c2),{c5}:] c= c3 ) ;
E14: [#] c2 is compact by COMPTS_1:10;
Int c3 = c3 by TOPS_1:55;
then c3 is a_neighborhood of [:([#] c2),{c5}:] by E13, CONNSP_2:def 2;
then consider c6 being a_neighborhood of [#] c2, c7 being a_neighborhood of c5 such that
E15: [:c6,c7:] c= c3 by E14, BORSUK_1:67;
take c8 = Int c7;
E16: ( Int c6 c= c6 & Int c7 c= c7 ) by TOPS_1:44;
[#] c2 c= Int c6 by CONNSP_2:def 2;
then E17: [#] c2 c= c6 by E16, XBOOLE_1:1;
c8 c= { b1 where B is Point of c1 : [:([#] c2),{b1}:] c= c3 }
proof
let c9 be set ; :: uses TARSKI:def 3
assume E18: c9 in c8 ;
then reconsider c10 = c9 as Point of c1 ;
{c9} c= c7 by E16, E18, ZFMISC_1:37;
then [:([#] c2),{c10}:] c= [:c6,c7:] by E17, ZFMISC_1:119;
then [:([#] c2),{c10}:] c= c3 by E15, XBOOLE_1:1;
hence c9 in { b1 where B is Point of c1 : [:([#] c2),{b1}:] c= c3 } ;
end;
hence ( c4 in c8 & c8 c= { b1 where B is Point of c1 : [:([#] c2),{b1}:] c= c3 } ) by E13, CONNSP_2:def 1;
end;

theorem E13: :: BORSUK_3:14
for b1 being non empty TopSpace
for b2 being non empty compact TopSpace
for b3 being open Subset of [:b2,b1:] holds { b4 where B is Point of b1 : [:([#] b2),{b4}:] c= b3 } in the topology of b1
proof
let c1 be non empty TopSpace;
let c2 be non empty compact TopSpace;
let c3 be open Subset of [:c2,c1:];
set c4 = { b1 where B is Point of c1 : [:([#] c2),{b1}:] c= c3 } ;
{ b1 where B is Point of c1 : [:([#] c2),{b1}:] c= c3 } c= the carrier of c1
proof
let c5 be set ; :: uses TARSKI:def 3
assume c5 in { b1 where B is Point of c1 : [:([#] c2),{b1}:] c= c3 } ;
then consider c6 being Point of c1 such that
E14: ( c5 = c6 & [:([#] c2),{c6}:] c= c3 ) ;
thus c5 in the carrier of c1 by E14;
end;
then reconsider c5 = { b1 where B is Point of c1 : [:([#] c2),{b1}:] c= c3 } as Subset of c1 ;
defpred S1[ set ] means ex b1 being set st
( b1 in c5 & ex b2 being Subset of c1 st
( b2 = a1 & b2 is open & b1 in b2 & b2 c= c5 ) );
consider c6 being set such that
E14: for b1 being set holds
( b1 in c6 iff ( b1 in bool c5 & S1[b1] ) ) from XBOOLE_0:sch 1();
 c6 c= bool c5
proof
let c7 be set ; :: uses TARSKI:def 3
assume c7 in c6 ;
hence c7 in bool c5 by E14;
end;
then reconsider c7 = c6 as Subset-Family of c5 ;
E15: union c7 = c5
proof
thus union c7 c= c5 ; :: uses XBOOLE_0:def 10
thus c5 c= union c7
proof
let c8 be set ; :: uses TARSKI:def 3
assume c8 in c5 ;
then consider c9 being open Subset of c1 such that
E16: ( c8 in c9 & c9 c= c5 ) by E12;
c9 in c7 by E14, E16;
hence c8 in union c7 by E16, TARSKI:def 4;
end;
end;
bool c5 c= bool the carrier of c1 by ZFMISC_1:79;
then reconsider c8 = c7 as Subset-Family of c1 by XBOOLE_1:1;
c8 c= the topology of c1
proof
let c9 be set ; :: uses TARSKI:def 3
assume c9 in c8 ;
then consider c10 being set such that
E16: ( c10 in c5 & ex b1 being Subset of c1 st
( b1 = c9 & b1 is open & c10 in b1 & b1 c= c5 ) ) by E14;
consider c11 being Subset of c1 such that
E17: ( c11 = c9 & c11 is open & c10 in c11 & c11 c= c5 ) by E16;
thus c9 in the topology of c1 by E17, PRE_TOPC:def 5;
end;
hence { b1 where B is Point of c1 : [:([#] c2),{b1}:] c= c3 } in the topology of c1 by E15, PRE_TOPC:def 1;
end;

theorem E14: :: BORSUK_3:15
for b1, b2 being non empty TopSpace
for b3 being Point of b1 holds [:(b1 | {b3}),b2:],b2 are_homeomorphic
proof
let c1, c2 be non empty TopSpace;
let c3 be Point of c1;
set c4 = {c3};
the carrier of [:(c1 | {c3}),c2:] = [:the carrier of (c1 | {c3}),the carrier of c2:] by BORSUK_1:def 5
.= [:{c3},the carrier of c2:] by JORDAN1:1 ;
then reconsider c5 = pr2 {c3},the carrier of c2 as Function of [:(c1 | {c3}),c2:],c2 ;
take c5 ; :: uses T_0TOPSP:def 1
thus c5 is being_homeomorphism by E11;
end;

E15: for b1, b2 being non empty TopSpace
for b3 being Point of b1
for b4 being non empty Subset of b1 holds
( b4 = {b3} implies [:b2,(b1 | b4):],b2 are_homeomorphic )
proof
let c1, c2 be non empty TopSpace;
let c3 be Point of c1;
let c4 be non empty Subset of c1;
assume c4 = {c3} ;
then E16: [:(c1 | c4),c2:],c2 are_homeomorphic by E14;
E17: [:c2,(c1 | c4):],[:(c1 | c4),c2:] are_homeomorphic by YELLOW12:44;
consider c5 being Function of [:(c1 | c4),c2:],c2 such that
E18: c5 is is_homeomorphism by E16, T_0TOPSP:def 1;
consider c6 being Function of [:c2,(c1 | c4):],[:(c1 | c4),c2:] such that
E19: c6 is is_homeomorphism by E17, T_0TOPSP:def 1;
reconsider c7 = c5 * c6 as Function of [:c2,(c1 | c4):],c2 ;
c7 is is_homeomorphism by E18, E19, TOPS_2:71;
hence [:c2,(c1 | c4):],c2 are_homeomorphic by T_0TOPSP:def 1;
end;

theorem E16: :: BORSUK_3:16
for b1, b2 being non empty TopSpace holds
( ( b1,b2 are_homeomorphic & b1 is compact ) implies ( b2 is compact ) )
proof
let c1, c2 be non empty TopSpace;
assume E17: ( c1,c2 are_homeomorphic & c1 is compact ) ;
then consider c3 being Function of c1,c2 such that
E18: c3 is is_homeomorphism by T_0TOPSP:def 1;
( c3 is continuous & rng c3 = [#] c2 ) by E18, TOPS_2:def 5;
hence c2 is compact by E17, COMPTS_1:23;
end;

theorem E17: :: BORSUK_3:17
for b1, b2 being TopSpace
for b3 being SubSpace of b1 holds
[:b2,b3:] is SubSpace of [:b2,b1:]
proof
let c1, c2 be TopSpace;
let c3 be SubSpace of c1;
set c4 = [:c2,c3:];
set c5 = [:c2,c1:];
E18: the carrier of [:c2,c3:] = [:the carrier of c2,the carrier of c3:] by BORSUK_1:def 5;
E19: the carrier of [:c2,c1:] = [:the carrier of c2,the carrier of c1:] by BORSUK_1:def 5;
E20: the carrier of c3 c= the carrier of c1 by BORSUK_1:35;
E21: ( the carrier of [:c2,c3:] = [#] [:c2,c3:] & the carrier of [:c2,c1:] = [#] [:c2,c1:] ) by PRE_TOPC:12;
then E22: [#] [:c2,c3:] c= [#] [:c2,c1:] by E18, E19, E20, ZFMISC_1:119;
for b1 being Subset of [:c2,c3:] holds
( b1 in the topology of [:c2,c3:] iff ex b2 being Subset of [:c2,c1:] st
( b2 in the topology of [:c2,c1:] & b1 = b2 /\ ([#] [:c2,c3:]) ) )
proof
let c6 be Subset of [:c2,c3:];
reconsider c7 = c6 as Subset of [:c2,c3:] ;
hereby
assume c6 in the topology of [:c2,c3:] ;
then c7 is open by PRE_TOPC:def 5;
then consider c8 being Subset-Family of [:c2,c3:] such that
E23: ( c7 = union c8 & for b1 being set holds
not ( b1 in c8 & for b2 being Subset of c2
for b3 being Subset of c3 holds
not ( b1 = [:b2,b3:] & b2 is open & b3 is open ) ) ) by BORSUK_1:45;
set c9 = { [:b1,b2:] where B is Subset of c2, B is Subset of c1 : ex b1 being Subset of c3 st
( b3 = b2 /\ ([#] c3) & b1 is open & b2 is open & [:b1,b3:] in c8 ) } ;
{ [:b1,b2:] where B is Subset of c2, B is Subset of c1 : ex b1 being Subset of c3 st
( b3 = b2 /\ ([#] c3) & b1 is open & b2 is open & [:b1,b3:] in c8 ) } c= bool the carrier of [:c2,c1:]
proof
let c10 be set ; :: uses TARSKI:def 3
assume c10 in { [:b1,b2:] where B is Subset of c2, B is Subset of c1 : ex b1 being Subset of c3 st
( b3