set L = Closed-Interval-TSpace (0,1);

let UL be Subset-Family of (Tunit_circle 2); :: thesis: ( UL is Cover of (Tunit_circle 2) & UL is open implies for Y being non empty TopSpace

for F being continuous Function of [:Y,I[01]:],(Tunit_circle 2)

for y being Point of Y ex T being non empty FinSequence of REAL st

( T . 1 = 0 & T . (len T) = 1 & T is increasing & ex N being open Subset of Y st

( y in N & ( for i being Nat st i in dom T & i + 1 in dom T holds

ex Ui being non empty Subset of (Tunit_circle 2) st

( Ui in UL & F .: [:N,[.(T . i),(T . (i + 1)).]:] c= Ui ) ) ) ) )

assume that

A1: UL is Cover of (Tunit_circle 2) and

A2: UL is open ; :: thesis: for Y being non empty TopSpace

for F being continuous Function of [:Y,I[01]:],(Tunit_circle 2)

for y being Point of Y ex T being non empty FinSequence of REAL st

( T . 1 = 0 & T . (len T) = 1 & T is increasing & ex N being open Subset of Y st

( y in N & ( for i being Nat st i in dom T & i + 1 in dom T holds

ex Ui being non empty Subset of (Tunit_circle 2) st

( Ui in UL & F .: [:N,[.(T . i),(T . (i + 1)).]:] c= Ui ) ) ) )

let Y be non empty TopSpace; :: thesis: for F being continuous Function of [:Y,I[01]:],(Tunit_circle 2)

for y being Point of Y ex T being non empty FinSequence of REAL st

( T . 1 = 0 & T . (len T) = 1 & T is increasing & ex N being open Subset of Y st

( y in N & ( for i being Nat st i in dom T & i + 1 in dom T holds

ex Ui being non empty Subset of (Tunit_circle 2) st

( Ui in UL & F .: [:N,[.(T . i),(T . (i + 1)).]:] c= Ui ) ) ) )

let F be continuous Function of [:Y,I[01]:],(Tunit_circle 2); :: thesis: for y being Point of Y ex T being non empty FinSequence of REAL st

( T . 1 = 0 & T . (len T) = 1 & T is increasing & ex N being open Subset of Y st

( y in N & ( for i being Nat st i in dom T & i + 1 in dom T holds

ex Ui being non empty Subset of (Tunit_circle 2) st

( Ui in UL & F .: [:N,[.(T . i),(T . (i + 1)).]:] c= Ui ) ) ) )

let y be Point of Y; :: thesis: ex T being non empty FinSequence of REAL st

( T . 1 = 0 & T . (len T) = 1 & T is increasing & ex N being open Subset of Y st

( y in N & ( for i being Nat st i in dom T & i + 1 in dom T holds

ex Ui being non empty Subset of (Tunit_circle 2) st

( Ui in UL & F .: [:N,[.(T . i),(T . (i + 1)).]:] c= Ui ) ) ) )

A3: [#] (Tunit_circle 2) = union UL by A1, SETFAM_1:45;

A4: for i being Point of I[01] ex U being non empty open Subset of (Tunit_circle 2) st

( F . [y,i] in U & U in UL )

( F . [y,0[01]] in U & U in UL ) ;

then reconsider UL1 = UL as non empty set ;

set C = the carrier of Y;

defpred S_{1}[ set , set ] means ex V being open Subset of (Tunit_circle 2) st

( V in UL1 & F . [y,$1] in V & $2 = V );

A6: for i being Element of the carrier of I[01] ex z being Element of UL1 st S_{1}[i,z]

A7: for i being Element of the carrier of I[01] holds S_{1}[i,I0 . i]
from FUNCT_2:sch 3(A6);

defpred S_{2}[ object , object ] means ex M being open Subset of Y ex O being open connected Subset of I[01] st

( y in M & $1 in O & F .: [:M,O:] c= I0 . $1 & $2 = [:M,O:] );

A8: for i being Element of the carrier of I[01] ex z being Subset of [: the carrier of Y, the carrier of I[01]:] st S_{2}[i,z]

A24: for i being Element of the carrier of I[01] holds S_{2}[i,I1 . i]
from FUNCT_2:sch 3(A8);

reconsider C1 = rng I1 as Subset-Family of [:Y,I[01]:] by BORSUK_1:def 2;

A25: C1 is open

[:{y},([#] I[01]):] c= union C1

[:{y},([#] I[01]):] is compact by BORSUK_3:23;

then consider G being Subset-Family of [:Y,I[01]:] such that

A36: G c= C1 and

A37: G is Cover of [:{y},([#] I[01]):] and

A38: G is finite by A35, A25;

set NN = { M where M is open Subset of Y : ( y in M & ex O being open Subset of I[01] st [:M,O:] in G ) } ;

{ M where M is open Subset of Y : ( y in M & ex O being open Subset of I[01] st [:M,O:] in G ) } c= bool the carrier of Y

consider p being Function such that

A39: rng p = G and

A40: dom p in omega by A38, FINSET_1:def 1;

defpred S_{3}[ object , object ] means ex M being open Subset of Y ex O being non empty open Subset of I[01] st

( y in M & p . $1 = [:M,O:] & $2 = M );

A41: for x being object st x in dom p holds

ex y being object st

( y in NN & S_{3}[x,y] )

A47: for x being object st x in dom p holds

S_{3}[x,p1 . x]
from FUNCT_2:sch 1(A41);

set ICOV = { O where O is open connected Subset of I[01] : ex M being open Subset of Y st [:M,O:] in G } ;

A48: [:{y},([#] I[01]):] c= union G by A37, SETFAM_1:def 11;

A49: y in {y} by TARSKI:def 1;

then [y,0[01]] in [:{y},([#] I[01]):] by ZFMISC_1:def 2;

then consider Z being set such that

[y,0[01]] in Z and

A50: Z in G by A48, TARSKI:def 4;

consider i being object such that

A51: i in dom I1 and

A52: I1 . i = Z by A36, A50, FUNCT_1:def 3;

consider M being open Subset of Y, O being open connected Subset of I[01] such that

A53: y in M and

i in O and

F .: [:M,O:] c= I0 . i and

A54: I1 . i = [:M,O:] by A24, A51;

A55: M in NN by A50, A52, A53, A54;

then A56: dom p1 = dom p by FUNCT_2:def 1;

rng p1 = NN

NN is open

{ O where O is open connected Subset of I[01] : ex M being open Subset of Y st [:M,O:] in G } c= bool the carrier of I[01]

[#] (Closed-Interval-TSpace (0,1)) c= union ICOV

set NCOV = the IntervalCover of ICOV;

set T = the IntervalCoverPts of the IntervalCover of ICOV;

A71: ICOV is connected

take T ; :: thesis: ( T . 1 = 0 & T . (len T) = 1 & T is increasing & ex N being open Subset of Y st

( y in N & ( for i being Nat st i in dom T & i + 1 in dom T holds

ex Ui being non empty Subset of (Tunit_circle 2) st

( Ui in UL & F .: [:N,[.(T . i),(T . (i + 1)).]:] c= Ui ) ) ) )

thus ( T . 1 = 0 & T . (len T) = 1 ) by A70, A72, A71, RCOMP_3:def 3; :: thesis: ( T is increasing & ex N being open Subset of Y st

( y in N & ( for i being Nat st i in dom T & i + 1 in dom T holds

ex Ui being non empty Subset of (Tunit_circle 2) st

( Ui in UL & F .: [:N,[.(T . i),(T . (i + 1)).]:] c= Ui ) ) ) )

thus T is increasing by A70, A72, A71, RCOMP_3:65; :: thesis: ex N being open Subset of Y st

( y in N & ( for i being Nat st i in dom T & i + 1 in dom T holds

ex Ui being non empty Subset of (Tunit_circle 2) st

( Ui in UL & F .: [:N,[.(T . i),(T . (i + 1)).]:] c= Ui ) ) )

take N ; :: thesis: ( y in N & ( for i being Nat st i in dom T & i + 1 in dom T holds

ex Ui being non empty Subset of (Tunit_circle 2) st

( Ui in UL & F .: [:N,[.(T . i),(T . (i + 1)).]:] c= Ui ) ) )

ex Ui being non empty Subset of (Tunit_circle 2) st

( Ui in UL & F .: [:N,[.(T . i),(T . (i + 1)).]:] c= Ui )

let i be Nat; :: thesis: ( i in dom T & i + 1 in dom T implies ex Ui being non empty Subset of (Tunit_circle 2) st

( Ui in UL & F .: [:N,[.(T . i),(T . (i + 1)).]:] c= Ui ) )

assume that

A73: i in dom T and

A74: i + 1 in dom T ; :: thesis: ex Ui being non empty Subset of (Tunit_circle 2) st

( Ui in UL & F .: [:N,[.(T . i),(T . (i + 1)).]:] c= Ui )

A75: 1 <= i by A73, FINSEQ_3:25;

A76: i + 1 <= len T by A74, FINSEQ_3:25;

len T = (len the IntervalCover of ICOV) + 1 by A70, A72, A71, RCOMP_3:def 3;

then i <= len the IntervalCover of ICOV by A76, XREAL_1:6;

then i in dom the IntervalCover of ICOV by A75, FINSEQ_3:25;

then A77: the IntervalCover of ICOV . i in rng the IntervalCover of ICOV by FUNCT_1:def 3;

rng the IntervalCover of ICOV c= ICOV by A70, A72, A71, RCOMP_3:def 2;

then the IntervalCover of ICOV . i in ICOV by A77;

then consider O being open connected Subset of I[01] such that

A78: the IntervalCover of ICOV . i = O and

A79: ex M being open Subset of Y st [:M,O:] in G ;

consider M being open Subset of Y such that

A80: [:M,O:] in G by A79;

i < len T by A76, NAT_1:13;

then A81: [.(T . i),(T . (i + 1)).] c= O by A70, A72, A71, A75, A78, RCOMP_3:66;

consider j being object such that

A82: j in dom I1 and

A83: I1 . j = [:M,O:] by A36, A80, FUNCT_1:def 3;

consider V being open Subset of (Tunit_circle 2) such that

A84: V in UL1 and

A85: F . [y,j] in V and

A86: I0 . j = V by A7, A82;

reconsider V = V as non empty open Subset of (Tunit_circle 2) by A85;

take V ; :: thesis: ( V in UL & F .: [:N,[.(T . i),(T . (i + 1)).]:] c= V )

thus V in UL by A84; :: thesis: F .: [:N,[.(T . i),(T . (i + 1)).]:] c= V

consider M1 being open Subset of Y, O1 being open connected Subset of I[01] such that

A87: y in M1 and

A88: j in O1 and

A89: F .: [:M1,O1:] c= I0 . j and

A90: I1 . j = [:M1,O1:] by A24, A82;

M = M1 by A83, A87, A88, A90, ZFMISC_1:110;

then M in NN by A80, A87;

then N c= M by SETFAM_1:3;

then [:N,[.(T . i),(T . (i + 1)).]:] c= [:M1,O1:] by A83, A90, A81, ZFMISC_1:96;

then F .: [:N,[.(T . i),(T . (i + 1)).]:] c= F .: [:M1,O1:] by RELAT_1:123;

hence F .: [:N,[.(T . i),(T . (i + 1)).]:] c= V by A89, A86; :: thesis: verum

let UL be Subset-Family of (Tunit_circle 2); :: thesis: ( UL is Cover of (Tunit_circle 2) & UL is open implies for Y being non empty TopSpace

for F being continuous Function of [:Y,I[01]:],(Tunit_circle 2)

for y being Point of Y ex T being non empty FinSequence of REAL st

( T . 1 = 0 & T . (len T) = 1 & T is increasing & ex N being open Subset of Y st

( y in N & ( for i being Nat st i in dom T & i + 1 in dom T holds

ex Ui being non empty Subset of (Tunit_circle 2) st

( Ui in UL & F .: [:N,[.(T . i),(T . (i + 1)).]:] c= Ui ) ) ) ) )

assume that

A1: UL is Cover of (Tunit_circle 2) and

A2: UL is open ; :: thesis: for Y being non empty TopSpace

for F being continuous Function of [:Y,I[01]:],(Tunit_circle 2)

for y being Point of Y ex T being non empty FinSequence of REAL st

( T . 1 = 0 & T . (len T) = 1 & T is increasing & ex N being open Subset of Y st

( y in N & ( for i being Nat st i in dom T & i + 1 in dom T holds

ex Ui being non empty Subset of (Tunit_circle 2) st

( Ui in UL & F .: [:N,[.(T . i),(T . (i + 1)).]:] c= Ui ) ) ) )

let Y be non empty TopSpace; :: thesis: for F being continuous Function of [:Y,I[01]:],(Tunit_circle 2)

for y being Point of Y ex T being non empty FinSequence of REAL st

( T . 1 = 0 & T . (len T) = 1 & T is increasing & ex N being open Subset of Y st

( y in N & ( for i being Nat st i in dom T & i + 1 in dom T holds

ex Ui being non empty Subset of (Tunit_circle 2) st

( Ui in UL & F .: [:N,[.(T . i),(T . (i + 1)).]:] c= Ui ) ) ) )

let F be continuous Function of [:Y,I[01]:],(Tunit_circle 2); :: thesis: for y being Point of Y ex T being non empty FinSequence of REAL st

( T . 1 = 0 & T . (len T) = 1 & T is increasing & ex N being open Subset of Y st

( y in N & ( for i being Nat st i in dom T & i + 1 in dom T holds

ex Ui being non empty Subset of (Tunit_circle 2) st

( Ui in UL & F .: [:N,[.(T . i),(T . (i + 1)).]:] c= Ui ) ) ) )

let y be Point of Y; :: thesis: ex T being non empty FinSequence of REAL st

( T . 1 = 0 & T . (len T) = 1 & T is increasing & ex N being open Subset of Y st

( y in N & ( for i being Nat st i in dom T & i + 1 in dom T holds

ex Ui being non empty Subset of (Tunit_circle 2) st

( Ui in UL & F .: [:N,[.(T . i),(T . (i + 1)).]:] c= Ui ) ) ) )

A3: [#] (Tunit_circle 2) = union UL by A1, SETFAM_1:45;

A4: for i being Point of I[01] ex U being non empty open Subset of (Tunit_circle 2) st

( F . [y,i] in U & U in UL )

proof

then
ex U being non empty open Subset of (Tunit_circle 2) st
let i be Point of I[01]; :: thesis: ex U being non empty open Subset of (Tunit_circle 2) st

( F . [y,i] in U & U in UL )

consider U being set such that

A5: ( F . [y,i] in U & U in UL ) by A3, TARSKI:def 4;

reconsider U = U as non empty open Subset of (Tunit_circle 2) by A2, A5;

take U ; :: thesis: ( F . [y,i] in U & U in UL )

thus ( F . [y,i] in U & U in UL ) by A5; :: thesis: verum

end;( F . [y,i] in U & U in UL )

consider U being set such that

A5: ( F . [y,i] in U & U in UL ) by A3, TARSKI:def 4;

reconsider U = U as non empty open Subset of (Tunit_circle 2) by A2, A5;

take U ; :: thesis: ( F . [y,i] in U & U in UL )

thus ( F . [y,i] in U & U in UL ) by A5; :: thesis: verum

( F . [y,0[01]] in U & U in UL ) ;

then reconsider UL1 = UL as non empty set ;

set C = the carrier of Y;

defpred S

( V in UL1 & F . [y,$1] in V & $2 = V );

A6: for i being Element of the carrier of I[01] ex z being Element of UL1 st S

proof

consider I0 being Function of the carrier of I[01],UL1 such that
let i be Element of the carrier of I[01]; :: thesis: ex z being Element of UL1 st S_{1}[i,z]

ex U being non empty open Subset of (Tunit_circle 2) st

( F . [y,i] in U & U in UL ) by A4;

hence ex z being Element of UL1 st S_{1}[i,z]
; :: thesis: verum

end;ex U being non empty open Subset of (Tunit_circle 2) st

( F . [y,i] in U & U in UL ) by A4;

hence ex z being Element of UL1 st S

A7: for i being Element of the carrier of I[01] holds S

defpred S

( y in M & $1 in O & F .: [:M,O:] c= I0 . $1 & $2 = [:M,O:] );

A8: for i being Element of the carrier of I[01] ex z being Subset of [: the carrier of Y, the carrier of I[01]:] st S

proof

consider I1 being Function of the carrier of I[01],(bool [: the carrier of Y, the carrier of I[01]:]) such that
let i be Element of the carrier of I[01]; :: thesis: ex z being Subset of [: the carrier of Y, the carrier of I[01]:] st S_{2}[i,z]

consider V being open Subset of (Tunit_circle 2) such that

V in UL1 and

A9: F . [y,i] in V and

A10: I0 . i = V by A7;

consider W being Subset of [:Y,I[01]:] such that

A11: [y,i] in W and

A12: W is open and

A13: F .: W c= V by A9, JGRAPH_2:10;

consider Q being Subset-Family of [:Y,I[01]:] such that

A14: W = union Q and

A15: for e being set st e in Q holds

ex A being Subset of Y ex B being Subset of I[01] st

( e = [:A,B:] & A is open & B is open ) by A12, BORSUK_1:5;

consider Z being set such that

A16: [y,i] in Z and

A17: Z in Q by A11, A14, TARSKI:def 4;

consider A being Subset of Y, B being Subset of I[01] such that

A18: Z = [:A,B:] and

A19: A is open and

A20: B is open by A15, A17;

reconsider A = A as open Subset of Y by A19;

A21: i in B by A16, A18, ZFMISC_1:87;

reconsider B = B as non empty open Subset of I[01] by A16, A18, A20;

reconsider i1 = i as Point of (I[01] | B) by A21, PRE_TOPC:8;

Component_of i1 is a_component by CONNSP_1:40;

then A22: Component_of i1 is open by CONNSP_2:15;

Component_of (i,B) = Component_of i1 by A21, CONNSP_3:def 7;

then reconsider D = Component_of (i,B) as open connected Subset of I[01] by A21, A22, CONNSP_3:33, TSEP_1:17;

reconsider z = [:A,D:] as Subset of [: the carrier of Y, the carrier of I[01]:] by BORSUK_1:def 2;

take z ; :: thesis: S_{2}[i,z]

take A ; :: thesis: ex O being open connected Subset of I[01] st

( y in A & i in O & F .: [:A,O:] c= I0 . i & z = [:A,O:] )

take D ; :: thesis: ( y in A & i in D & F .: [:A,D:] c= I0 . i & z = [:A,D:] )

thus y in A by A16, A18, ZFMISC_1:87; :: thesis: ( i in D & F .: [:A,D:] c= I0 . i & z = [:A,D:] )

thus i in D by A21, CONNSP_3:26; :: thesis: ( F .: [:A,D:] c= I0 . i & z = [:A,D:] )

D c= B by A21, Th3;

then A23: z c= [:A,B:] by ZFMISC_1:95;

[:A,B:] c= W by A14, A17, A18, ZFMISC_1:74;

then z c= W by A23;

then F .: z c= F .: W by RELAT_1:123;

hence F .: [:A,D:] c= I0 . i by A10, A13; :: thesis: z = [:A,D:]

thus z = [:A,D:] ; :: thesis: verum

end;consider V being open Subset of (Tunit_circle 2) such that

V in UL1 and

A9: F . [y,i] in V and

A10: I0 . i = V by A7;

consider W being Subset of [:Y,I[01]:] such that

A11: [y,i] in W and

A12: W is open and

A13: F .: W c= V by A9, JGRAPH_2:10;

consider Q being Subset-Family of [:Y,I[01]:] such that

A14: W = union Q and

A15: for e being set st e in Q holds

ex A being Subset of Y ex B being Subset of I[01] st

( e = [:A,B:] & A is open & B is open ) by A12, BORSUK_1:5;

consider Z being set such that

A16: [y,i] in Z and

A17: Z in Q by A11, A14, TARSKI:def 4;

consider A being Subset of Y, B being Subset of I[01] such that

A18: Z = [:A,B:] and

A19: A is open and

A20: B is open by A15, A17;

reconsider A = A as open Subset of Y by A19;

A21: i in B by A16, A18, ZFMISC_1:87;

reconsider B = B as non empty open Subset of I[01] by A16, A18, A20;

reconsider i1 = i as Point of (I[01] | B) by A21, PRE_TOPC:8;

Component_of i1 is a_component by CONNSP_1:40;

then A22: Component_of i1 is open by CONNSP_2:15;

Component_of (i,B) = Component_of i1 by A21, CONNSP_3:def 7;

then reconsider D = Component_of (i,B) as open connected Subset of I[01] by A21, A22, CONNSP_3:33, TSEP_1:17;

reconsider z = [:A,D:] as Subset of [: the carrier of Y, the carrier of I[01]:] by BORSUK_1:def 2;

take z ; :: thesis: S

take A ; :: thesis: ex O being open connected Subset of I[01] st

( y in A & i in O & F .: [:A,O:] c= I0 . i & z = [:A,O:] )

take D ; :: thesis: ( y in A & i in D & F .: [:A,D:] c= I0 . i & z = [:A,D:] )

thus y in A by A16, A18, ZFMISC_1:87; :: thesis: ( i in D & F .: [:A,D:] c= I0 . i & z = [:A,D:] )

thus i in D by A21, CONNSP_3:26; :: thesis: ( F .: [:A,D:] c= I0 . i & z = [:A,D:] )

D c= B by A21, Th3;

then A23: z c= [:A,B:] by ZFMISC_1:95;

[:A,B:] c= W by A14, A17, A18, ZFMISC_1:74;

then z c= W by A23;

then F .: z c= F .: W by RELAT_1:123;

hence F .: [:A,D:] c= I0 . i by A10, A13; :: thesis: z = [:A,D:]

thus z = [:A,D:] ; :: thesis: verum

A24: for i being Element of the carrier of I[01] holds S

reconsider C1 = rng I1 as Subset-Family of [:Y,I[01]:] by BORSUK_1:def 2;

A25: C1 is open

proof

A28:
dom I1 = the carrier of I[01]
by FUNCT_2:def 1;
let P be Subset of [:Y,I[01]:]; :: according to TOPS_2:def 1 :: thesis: ( not P in C1 or P is open )

assume P in C1 ; :: thesis: P is open

then consider i being object such that

A26: i in dom I1 and

A27: I1 . i = P by FUNCT_1:def 3;

S_{2}[i,I1 . i]
by A24, A26;

hence P is open by A27, BORSUK_1:6; :: thesis: verum

end;assume P in C1 ; :: thesis: P is open

then consider i being object such that

A26: i in dom I1 and

A27: I1 . i = P by FUNCT_1:def 3;

S

hence P is open by A27, BORSUK_1:6; :: thesis: verum

[:{y},([#] I[01]):] c= union C1

proof

then A35:
C1 is Cover of [:{y},([#] I[01]):]
by SETFAM_1:def 11;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in [:{y},([#] I[01]):] or a in union C1 )

assume a in [:{y},([#] I[01]):] ; :: thesis: a in union C1

then consider a1, a2 being object such that

A29: a1 in {y} and

A30: a2 in [#] I[01] and

A31: a = [a1,a2] by ZFMISC_1:def 2;

A32: a1 = y by A29, TARSKI:def 1;

reconsider a2 = a2 as Point of I[01] by A30;

consider M being open Subset of Y, O being open connected Subset of I[01] such that

A33: ( y in M & a2 in O ) and

F .: [:M,O:] c= I0 . a2 and

A34: I1 . a2 = [:M,O:] by A24;

( [y,a2] in [:M,O:] & [:M,O:] in C1 ) by A28, A33, A34, FUNCT_1:def 3, ZFMISC_1:87;

hence a in union C1 by A31, A32, TARSKI:def 4; :: thesis: verum

end;assume a in [:{y},([#] I[01]):] ; :: thesis: a in union C1

then consider a1, a2 being object such that

A29: a1 in {y} and

A30: a2 in [#] I[01] and

A31: a = [a1,a2] by ZFMISC_1:def 2;

A32: a1 = y by A29, TARSKI:def 1;

reconsider a2 = a2 as Point of I[01] by A30;

consider M being open Subset of Y, O being open connected Subset of I[01] such that

A33: ( y in M & a2 in O ) and

F .: [:M,O:] c= I0 . a2 and

A34: I1 . a2 = [:M,O:] by A24;

( [y,a2] in [:M,O:] & [:M,O:] in C1 ) by A28, A33, A34, FUNCT_1:def 3, ZFMISC_1:87;

hence a in union C1 by A31, A32, TARSKI:def 4; :: thesis: verum

[:{y},([#] I[01]):] is compact by BORSUK_3:23;

then consider G being Subset-Family of [:Y,I[01]:] such that

A36: G c= C1 and

A37: G is Cover of [:{y},([#] I[01]):] and

A38: G is finite by A35, A25;

set NN = { M where M is open Subset of Y : ( y in M & ex O being open Subset of I[01] st [:M,O:] in G ) } ;

{ M where M is open Subset of Y : ( y in M & ex O being open Subset of I[01] st [:M,O:] in G ) } c= bool the carrier of Y

proof

then reconsider NN = { M where M is open Subset of Y : ( y in M & ex O being open Subset of I[01] st [:M,O:] in G ) } as Subset-Family of Y ;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { M where M is open Subset of Y : ( y in M & ex O being open Subset of I[01] st [:M,O:] in G ) } or a in bool the carrier of Y )

assume a in { M where M is open Subset of Y : ( y in M & ex O being open Subset of I[01] st [:M,O:] in G ) } ; :: thesis: a in bool the carrier of Y

then ex M being open Subset of Y st

( a = M & y in M & ex O being open Subset of I[01] st [:M,O:] in G ) ;

hence a in bool the carrier of Y ; :: thesis: verum

end;assume a in { M where M is open Subset of Y : ( y in M & ex O being open Subset of I[01] st [:M,O:] in G ) } ; :: thesis: a in bool the carrier of Y

then ex M being open Subset of Y st

( a = M & y in M & ex O being open Subset of I[01] st [:M,O:] in G ) ;

hence a in bool the carrier of Y ; :: thesis: verum

consider p being Function such that

A39: rng p = G and

A40: dom p in omega by A38, FINSET_1:def 1;

defpred S

( y in M & p . $1 = [:M,O:] & $2 = M );

A41: for x being object st x in dom p holds

ex y being object st

( y in NN & S

proof

consider p1 being Function of (dom p),NN such that
let x be object ; :: thesis: ( x in dom p implies ex y being object st

( y in NN & S_{3}[x,y] ) )

assume x in dom p ; :: thesis: ex y being object st

( y in NN & S_{3}[x,y] )

then A42: p . x in rng p by FUNCT_1:def 3;

then consider i being object such that

A43: i in dom I1 and

A44: I1 . i = p . x by A36, A39, FUNCT_1:def 3;

consider M being open Subset of Y, O being open connected Subset of I[01] such that

A45: ( y in M & i in O ) and

F .: [:M,O:] c= I0 . i and

A46: I1 . i = [:M,O:] by A24, A43;

take M ; :: thesis: ( M in NN & S_{3}[x,M] )

thus ( M in NN & S_{3}[x,M] )
by A39, A42, A44, A45, A46; :: thesis: verum

end;( y in NN & S

assume x in dom p ; :: thesis: ex y being object st

( y in NN & S

then A42: p . x in rng p by FUNCT_1:def 3;

then consider i being object such that

A43: i in dom I1 and

A44: I1 . i = p . x by A36, A39, FUNCT_1:def 3;

consider M being open Subset of Y, O being open connected Subset of I[01] such that

A45: ( y in M & i in O ) and

F .: [:M,O:] c= I0 . i and

A46: I1 . i = [:M,O:] by A24, A43;

take M ; :: thesis: ( M in NN & S

thus ( M in NN & S

A47: for x being object st x in dom p holds

S

set ICOV = { O where O is open connected Subset of I[01] : ex M being open Subset of Y st [:M,O:] in G } ;

A48: [:{y},([#] I[01]):] c= union G by A37, SETFAM_1:def 11;

A49: y in {y} by TARSKI:def 1;

then [y,0[01]] in [:{y},([#] I[01]):] by ZFMISC_1:def 2;

then consider Z being set such that

[y,0[01]] in Z and

A50: Z in G by A48, TARSKI:def 4;

consider i being object such that

A51: i in dom I1 and

A52: I1 . i = Z by A36, A50, FUNCT_1:def 3;

consider M being open Subset of Y, O being open connected Subset of I[01] such that

A53: y in M and

i in O and

F .: [:M,O:] c= I0 . i and

A54: I1 . i = [:M,O:] by A24, A51;

A55: M in NN by A50, A52, A53, A54;

then A56: dom p1 = dom p by FUNCT_2:def 1;

rng p1 = NN

proof

then A64:
NN is finite
by A40, A56, FINSET_1:def 1;
thus
rng p1 c= NN
; :: according to XBOOLE_0:def 10 :: thesis: NN c= rng p1

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in NN or a in rng p1 )

assume a in NN ; :: thesis: a in rng p1

then consider M being open Subset of Y such that

A57: a = M and

y in M and

A58: ex O being open Subset of I[01] st [:M,O:] in G ;

consider O being open Subset of I[01] such that

A59: [:M,O:] in G by A58;

consider b being object such that

A60: b in dom p and

A61: p . b = [:M,O:] by A39, A59, FUNCT_1:def 3;

consider M1 being open Subset of Y, O1 being non empty open Subset of I[01] such that

A62: ( y in M1 & p . b = [:M1,O1:] ) and

A63: p1 . b = M1 by A47, A60;

M1 = M by A61, A62, ZFMISC_1:110;

hence a in rng p1 by A56, A57, A60, A63, FUNCT_1:def 3; :: thesis: verum

end;let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in NN or a in rng p1 )

assume a in NN ; :: thesis: a in rng p1

then consider M being open Subset of Y such that

A57: a = M and

y in M and

A58: ex O being open Subset of I[01] st [:M,O:] in G ;

consider O being open Subset of I[01] such that

A59: [:M,O:] in G by A58;

consider b being object such that

A60: b in dom p and

A61: p . b = [:M,O:] by A39, A59, FUNCT_1:def 3;

consider M1 being open Subset of Y, O1 being non empty open Subset of I[01] such that

A62: ( y in M1 & p . b = [:M1,O1:] ) and

A63: p1 . b = M1 by A47, A60;

M1 = M by A61, A62, ZFMISC_1:110;

hence a in rng p1 by A56, A57, A60, A63, FUNCT_1:def 3; :: thesis: verum

NN is open

proof

then reconsider N = meet NN as open Subset of Y by A64, TOPS_2:20;
let a be Subset of Y; :: according to TOPS_2:def 1 :: thesis: ( not a in NN or a is open )

assume a in NN ; :: thesis: a is open

then ex M being open Subset of Y st

( a = M & y in M & ex O being open Subset of I[01] st [:M,O:] in G ) ;

hence a is open ; :: thesis: verum

end;assume a in NN ; :: thesis: a is open

then ex M being open Subset of Y st

( a = M & y in M & ex O being open Subset of I[01] st [:M,O:] in G ) ;

hence a is open ; :: thesis: verum

{ O where O is open connected Subset of I[01] : ex M being open Subset of Y st [:M,O:] in G } c= bool the carrier of I[01]

proof

then reconsider ICOV = { O where O is open connected Subset of I[01] : ex M being open Subset of Y st [:M,O:] in G } as Subset-Family of (Closed-Interval-TSpace (0,1)) by TOPMETR:20;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { O where O is open connected Subset of I[01] : ex M being open Subset of Y st [:M,O:] in G } or a in bool the carrier of I[01] )

assume a in { O where O is open connected Subset of I[01] : ex M being open Subset of Y st [:M,O:] in G } ; :: thesis: a in bool the carrier of I[01]

then ex O being open connected Subset of I[01] st

( a = O & ex M being open Subset of Y st [:M,O:] in G ) ;

hence a in bool the carrier of I[01] ; :: thesis: verum

end;assume a in { O where O is open connected Subset of I[01] : ex M being open Subset of Y st [:M,O:] in G } ; :: thesis: a in bool the carrier of I[01]

then ex O being open connected Subset of I[01] st

( a = O & ex M being open Subset of Y st [:M,O:] in G ) ;

hence a in bool the carrier of I[01] ; :: thesis: verum

[#] (Closed-Interval-TSpace (0,1)) c= union ICOV

proof

then A70:
ICOV is Cover of (Closed-Interval-TSpace (0,1))
by SETFAM_1:def 11;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in [#] (Closed-Interval-TSpace (0,1)) or a in union ICOV )

assume a in [#] (Closed-Interval-TSpace (0,1)) ; :: thesis: a in union ICOV

then reconsider a = a as Point of I[01] by TOPMETR:20;

[y,a] in [:{y},([#] I[01]):] by A49, ZFMISC_1:def 2;

then consider Z being set such that

A65: [y,a] in Z and

A66: Z in G by A48, TARSKI:def 4;

consider i being object such that

A67: i in dom I1 and

A68: I1 . i = Z by A36, A66, FUNCT_1:def 3;

consider M being open Subset of Y, O being open connected Subset of I[01] such that

y in M and

i in O and

F .: [:M,O:] c= I0 . i and

A69: I1 . i = [:M,O:] by A24, A67;

( a in O & O in ICOV ) by A65, A66, A68, A69, ZFMISC_1:87;

hence a in union ICOV by TARSKI:def 4; :: thesis: verum

end;assume a in [#] (Closed-Interval-TSpace (0,1)) ; :: thesis: a in union ICOV

then reconsider a = a as Point of I[01] by TOPMETR:20;

[y,a] in [:{y},([#] I[01]):] by A49, ZFMISC_1:def 2;

then consider Z being set such that

A65: [y,a] in Z and

A66: Z in G by A48, TARSKI:def 4;

consider i being object such that

A67: i in dom I1 and

A68: I1 . i = Z by A36, A66, FUNCT_1:def 3;

consider M being open Subset of Y, O being open connected Subset of I[01] such that

y in M and

i in O and

F .: [:M,O:] c= I0 . i and

A69: I1 . i = [:M,O:] by A24, A67;

( a in O & O in ICOV ) by A65, A66, A68, A69, ZFMISC_1:87;

hence a in union ICOV by TARSKI:def 4; :: thesis: verum

set NCOV = the IntervalCover of ICOV;

set T = the IntervalCoverPts of the IntervalCover of ICOV;

A71: ICOV is connected

proof

A72:
ICOV is open
let X be Subset of (Closed-Interval-TSpace (0,1)); :: according to RCOMP_3:def 1 :: thesis: ( not X in ICOV or X is connected )

assume X in ICOV ; :: thesis: X is connected

then ex O being open connected Subset of I[01] st

( X = O & ex M being open Subset of Y st [:M,O:] in G ) ;

hence X is connected by TOPMETR:20; :: thesis: verum

end;assume X in ICOV ; :: thesis: X is connected

then ex O being open connected Subset of I[01] st

( X = O & ex M being open Subset of Y st [:M,O:] in G ) ;

hence X is connected by TOPMETR:20; :: thesis: verum

proof

then reconsider T = the IntervalCoverPts of the IntervalCover of ICOV as non empty FinSequence of REAL by A70, A71, Lm15;
let a be Subset of (Closed-Interval-TSpace (0,1)); :: according to TOPS_2:def 1 :: thesis: ( not a in ICOV or a is open )

assume a in ICOV ; :: thesis: a is open

then ex O being open connected Subset of I[01] st

( a = O & ex M being open Subset of Y st [:M,O:] in G ) ;

hence a is open by TOPMETR:20; :: thesis: verum

end;assume a in ICOV ; :: thesis: a is open

then ex O being open connected Subset of I[01] st

( a = O & ex M being open Subset of Y st [:M,O:] in G ) ;

hence a is open by TOPMETR:20; :: thesis: verum

take T ; :: thesis: ( T . 1 = 0 & T . (len T) = 1 & T is increasing & ex N being open Subset of Y st

( y in N & ( for i being Nat st i in dom T & i + 1 in dom T holds

ex Ui being non empty Subset of (Tunit_circle 2) st

( Ui in UL & F .: [:N,[.(T . i),(T . (i + 1)).]:] c= Ui ) ) ) )

thus ( T . 1 = 0 & T . (len T) = 1 ) by A70, A72, A71, RCOMP_3:def 3; :: thesis: ( T is increasing & ex N being open Subset of Y st

( y in N & ( for i being Nat st i in dom T & i + 1 in dom T holds

ex Ui being non empty Subset of (Tunit_circle 2) st

( Ui in UL & F .: [:N,[.(T . i),(T . (i + 1)).]:] c= Ui ) ) ) )

thus T is increasing by A70, A72, A71, RCOMP_3:65; :: thesis: ex N being open Subset of Y st

( y in N & ( for i being Nat st i in dom T & i + 1 in dom T holds

ex Ui being non empty Subset of (Tunit_circle 2) st

( Ui in UL & F .: [:N,[.(T . i),(T . (i + 1)).]:] c= Ui ) ) )

take N ; :: thesis: ( y in N & ( for i being Nat st i in dom T & i + 1 in dom T holds

ex Ui being non empty Subset of (Tunit_circle 2) st

( Ui in UL & F .: [:N,[.(T . i),(T . (i + 1)).]:] c= Ui ) ) )

now :: thesis: for Z being set st Z in NN holds

y in Z

hence
y in N
by A55, SETFAM_1:def 1; :: thesis: for i being Nat st i in dom T & i + 1 in dom T holds y in Z

let Z be set ; :: thesis: ( Z in NN implies y in Z )

assume Z in NN ; :: thesis: y in Z

then ex M being open Subset of Y st

( Z = M & y in M & ex O being open Subset of I[01] st [:M,O:] in G ) ;

hence y in Z ; :: thesis: verum

end;assume Z in NN ; :: thesis: y in Z

then ex M being open Subset of Y st

( Z = M & y in M & ex O being open Subset of I[01] st [:M,O:] in G ) ;

hence y in Z ; :: thesis: verum

ex Ui being non empty Subset of (Tunit_circle 2) st

( Ui in UL & F .: [:N,[.(T . i),(T . (i + 1)).]:] c= Ui )

let i be Nat; :: thesis: ( i in dom T & i + 1 in dom T implies ex Ui being non empty Subset of (Tunit_circle 2) st

( Ui in UL & F .: [:N,[.(T . i),(T . (i + 1)).]:] c= Ui ) )

assume that

A73: i in dom T and

A74: i + 1 in dom T ; :: thesis: ex Ui being non empty Subset of (Tunit_circle 2) st

( Ui in UL & F .: [:N,[.(T . i),(T . (i + 1)).]:] c= Ui )

A75: 1 <= i by A73, FINSEQ_3:25;

A76: i + 1 <= len T by A74, FINSEQ_3:25;

len T = (len the IntervalCover of ICOV) + 1 by A70, A72, A71, RCOMP_3:def 3;

then i <= len the IntervalCover of ICOV by A76, XREAL_1:6;

then i in dom the IntervalCover of ICOV by A75, FINSEQ_3:25;

then A77: the IntervalCover of ICOV . i in rng the IntervalCover of ICOV by FUNCT_1:def 3;

rng the IntervalCover of ICOV c= ICOV by A70, A72, A71, RCOMP_3:def 2;

then the IntervalCover of ICOV . i in ICOV by A77;

then consider O being open connected Subset of I[01] such that

A78: the IntervalCover of ICOV . i = O and

A79: ex M being open Subset of Y st [:M,O:] in G ;

consider M being open Subset of Y such that

A80: [:M,O:] in G by A79;

i < len T by A76, NAT_1:13;

then A81: [.(T . i),(T . (i + 1)).] c= O by A70, A72, A71, A75, A78, RCOMP_3:66;

consider j being object such that

A82: j in dom I1 and

A83: I1 . j = [:M,O:] by A36, A80, FUNCT_1:def 3;

consider V being open Subset of (Tunit_circle 2) such that

A84: V in UL1 and

A85: F . [y,j] in V and

A86: I0 . j = V by A7, A82;

reconsider V = V as non empty open Subset of (Tunit_circle 2) by A85;

take V ; :: thesis: ( V in UL & F .: [:N,[.(T . i),(T . (i + 1)).]:] c= V )

thus V in UL by A84; :: thesis: F .: [:N,[.(T . i),(T . (i + 1)).]:] c= V

consider M1 being open Subset of Y, O1 being open connected Subset of I[01] such that

A87: y in M1 and

A88: j in O1 and

A89: F .: [:M1,O1:] c= I0 . j and

A90: I1 . j = [:M1,O1:] by A24, A82;

M = M1 by A83, A87, A88, A90, ZFMISC_1:110;

then M in NN by A80, A87;

then N c= M by SETFAM_1:3;

then [:N,[.(T . i),(T . (i + 1)).]:] c= [:M1,O1:] by A83, A90, A81, ZFMISC_1:96;

then F .: [:N,[.(T . i),(T . (i + 1)).]:] c= F .: [:M1,O1:] by RELAT_1:123;

hence F .: [:N,[.(T . i),(T . (i + 1)).]:] c= V by A89, A86; :: thesis: verum