for A, B being Subset of I[01] st [#] I[01] = A \/ B & A <> {} I[01] & B <> {} I[01] & A is closed & B is closed holds
A meets B

proof

let A, B be Subset of I[01]; :: thesis:
assume that
A1: [#] I[01] = A \/ B and
A2: A <> {} I[01] and
A3: B <> {} I[01] and
A4: A is closed and
A5: B is closed ; :: thesis:
reconsider P = A, Q = B as Subset of REAL by BORSUK_1:40, XBOOLE_1:1;
assume A6: A misses B ; :: thesis:
set x = the Element of P;
reconsider x = the Element of P as Real ;

A7: now :: thesis:

take x = x; :: thesis:
thus x in P by A2; :: thesis:

end;

set x = the Element of Q;
reconsider x = the Element of Q as Real ;

A8: now :: thesis:

take x = x; :: thesis:
thus x in Q by A3; :: thesis:

end;

A9: the carrier of RealSpace = the carrier of (TopSpaceMetr RealSpace) by TOPMETR:12;
0 is LowerBound of P

proof

let r be ExtReal; :: according to XXREAL_2:def 2 :: thesis:
assume r in P ; :: thesis:
then r in [.0,1.] by BORSUK_1:40;
then r in { w where w is Real : ( 0 <= w & w <= 1 ) } by RCOMP_1:def 1;
then ex u being Real st
( u = r & 0 <= u & u <= 1 ) ;
hence 0 <= r ; :: thesis:

end;

then A10: P is bounded_below ;
0 is LowerBound of Q

proof

let r be ExtReal; :: according to XXREAL_2:def 2 :: thesis:
assume r in Q ; :: thesis:
then r in [.0,1.] by BORSUK_1:40;
then r in { w where w is Real : ( 0 <= w & w <= 1 ) } by RCOMP_1:def 1;
then ex u being Real st
( u = r & 0 <= u & u <= 1 ) ;
hence 0 <= r ; :: thesis:

end;

then A11: Q is bounded_below ;
reconsider A0 = P, B0 = Q as Subset of R^1 by METRIC_1:def 13, TOPMETR:12, TOPMETR:def 6;
A12: I[01] is closed SubSpace of R^1 by Th2, TOPMETR:20;
then A13: A0 is closed by A4, TSEP_1:12;
A14: B0 is closed by A5, A12, TSEP_1:12;
0 in { w where w is Real : ( 0 <= w & w <= 1 ) } ;
then A15: 0 in [.0,1.] by RCOMP_1:def 1;

now :: thesis:

per cases by A1, A15, BORSUK_1:40, XBOOLE_0:def 3;

suppose A16: 0 in P ; :: thesis:

reconsider B00 = B0 ` as Subset of R^1 ;
set l = lower_bound Q;
lower_bound Q in REAL by XREAL_0:def 1;
then reconsider m = lower_bound Q as Point of RealSpace by METRIC_1:def 13;
reconsider t = m as Point of R^1 by TOPMETR:12, TOPMETR:def 6;
set W = { w where w is Real : ( 0 <= w & w < lower_bound Q ) } ;
A17: lower_bound Q in Q

proof

assume not lower_bound Q in Q ; :: thesis:
then A18: t in B00 by SUBSET_1:29;
B00 is open by A14, TOPS_1:3;
then consider s being Real such that
A19: s > 0 and
A20: Ball (m,s) c= B0 ` by A18, TOPMETR:15, TOPMETR:def 6;
consider r being Real such that
A21: r in Q and
A22: r < (lower_bound Q) + s by A8, A11, A19, SEQ_4:def 2;
reconsider r = r as Element of REAL by XREAL_0:def 1;
lower_bound Q <= r by A11, A21, SEQ_4:def 2;
then (lower_bound Q) - r <= 0 by XREAL_1:47;
then A23: - s < - ((lower_bound Q) - r) by A19, XREAL_1:24;
reconsider rm = r as Point of RealSpace by METRIC_1:def 13;
r - (lower_bound Q) < s by A22, XREAL_1:19;
then |.(r - (lower_bound Q)).| < s by A23, SEQ_2:1;
then the distance of RealSpace . (rm,m) < s by METRIC_1:def 12, METRIC_1:def 13;
then dist (m,rm) < s by METRIC_1:def 1;
then rm in { q where q is Element of RealSpace : dist (m,q) < s } ;
then rm in Ball (m,s) by METRIC_1:17;
hence contradiction by A20, A21, XBOOLE_0:def 5; :: thesis:

end;

then lower_bound Q in [.0,1.] by BORSUK_1:40;
then lower_bound Q in { u where u is Real : ( 0 <= u & u <= 1 ) } by RCOMP_1:def 1;
then A24: ex u0 being Real st
( u0 = lower_bound Q & 0 <= u0 & u0 <= 1 ) ;

now :: thesis:

let x be object ; :: thesis:
assume x in { w where w is Real : ( 0 <= w & w < lower_bound Q ) } ; :: thesis:
then consider w0 being Real such that
A25: w0 = x and
A26: 0 <= w0 and
A27: w0 < lower_bound Q ;
w0 <= 1 by A24, A27, XXREAL_0:2;
then w0 in { u where u is Real : ( 0 <= u & u <= 1 ) } by A26;
then w0 in P \/ Q by A1, BORSUK_1:40, RCOMP_1:def 1;
then ( w0 in P or w0 in Q ) by XBOOLE_0:def 3;
hence x in P by A11, A25, A27, SEQ_4:def 2; :: thesis:

end;

then A28: { w where w is Real : ( 0 <= w & w < lower_bound Q ) } c= P ;
then reconsider D = { w where w is Real : ( 0 <= w & w < lower_bound Q ) } as Subset of R^1 by A9, METRIC_1:def 13, TOPMETR:def 6, XBOOLE_1:1;
A29: not 0 in Q by A6, A16, XBOOLE_0:3;

now :: thesis:

let G be Subset of R^1; :: thesis:
assume A30: G is open ; :: thesis:
assume t in G ; :: thesis:
then consider e being Real such that
A31: e > 0 and
A32: Ball (m,e) c= G by A30, TOPMETR:15, TOPMETR:def 6;
reconsider e = e as Element of REAL by XREAL_0:def 1;
reconsider e0 = max (0,((lower_bound Q) - (e / 2))) as Element of REAL by XREAL_0:def 1;
reconsider e1 = e0 as Point of RealSpace by METRIC_1:def 13;
A33: e * (1 / 2) < e * 1 by A31, XREAL_1:68;

now :: thesis:

per cases by XXREAL_0:16;

suppose A34: e0 = 0 ; :: thesis:

then lower_bound Q <= e / 2 by XREAL_1:50, XXREAL_0:25;
then lower_bound Q < e by A33, XXREAL_0:2;
hence |.((lower_bound Q) - e0).| < e by A24, A34, ABSVALUE:def 1; :: thesis:

end;

suppose e0 = (lower_bound Q) - (e / 2) ; :: thesis:

hence |.((lower_bound Q) - e0).| < e by A31, A33, ABSVALUE:def 1; :: thesis:

end;

then the distance of RealSpace . (m,e1) < e by METRIC_1:def 12, METRIC_1:def 13;
then dist (m,e1) < e by METRIC_1:def 1;
then e1 in { z where z is Element of RealSpace : dist (m,z) < e } ;
then A35: e1 in Ball (m,e) by METRIC_1:17;
( e0 = 0 or e0 = (lower_bound Q) - (e / 2) ) by XXREAL_0:16;
then ( 0 <= e0 & e0 < lower_bound Q ) by A29, A17, A24, A31, XREAL_1:44, XREAL_1:139, XXREAL_0:25;
then e0 in { w where w is Real : ( 0 <= w & w < lower_bound Q ) } ;
hence D meets G by A32, A35, XBOOLE_0:3; :: thesis:

end;

then A36: t in Cl D by PRE_TOPC:24;
A37: Cl A0 = A0 by A13, PRE_TOPC:22;
Cl D c= Cl A0 by A28, PRE_TOPC:19;
hence contradiction by A6, A17, A36, A37, XBOOLE_0:3; :: thesis:

end;

suppose A38: 0 in Q ; :: thesis:

reconsider A00 = A0 ` as Subset of R^1 ;
set l = lower_bound P;
lower_bound P in REAL by XREAL_0:def 1;
then reconsider m = lower_bound P as Point of RealSpace by METRIC_1:def 13;
reconsider t = m as Point of R^1 by TOPMETR:12, TOPMETR:def 6;
set W = { w where w is Real : ( 0 <= w & w < lower_bound P ) } ;
A39: lower_bound P in P

proof

assume not lower_bound P in P ; :: thesis:
then A40: t in A00 by SUBSET_1:29;
A00 is open by A13, TOPS_1:3;
then consider s being Real such that
A41: s > 0 and
A42: Ball (m,s) c= A0 ` by A40, TOPMETR:15, TOPMETR:def 6;
consider r being Real such that
A43: r in P and
A44: r < (lower_bound P) + s by A7, A10, A41, SEQ_4:def 2;
reconsider r = r as Element of REAL by XREAL_0:def 1;
lower_bound P <= r by A10, A43, SEQ_4:def 2;
then (lower_bound P) - r <= 0 by XREAL_1:47;
then A45: - s < - ((lower_bound P) - r) by A41, XREAL_1:24;
reconsider rm = r as Point of RealSpace by METRIC_1:def 13;
A46: real_dist . (r,(lower_bound P)) = dist (rm,m) by METRIC_1:def 1, METRIC_1:def 13;
r - (lower_bound P) < s by A44, XREAL_1:19;
then |.(r - (lower_bound P)).| < s by A45, SEQ_2:1;
then dist (rm,m) < s by METRIC_1:def 12, A46;
then rm in { q where q is Element of RealSpace : dist (m,q) < s } ;
then rm in Ball (m,s) by METRIC_1:17;
hence contradiction by A42, A43, XBOOLE_0:def 5; :: thesis:

end;

then lower_bound P in [.0,1.] by BORSUK_1:40;
then lower_bound P in { u where u is Real : ( 0 <= u & u <= 1 ) } by RCOMP_1:def 1;
then A47: ex u0 being Real st
( u0 = lower_bound P & 0 <= u0 & u0 <= 1 ) ;

now :: thesis:

let x be object ; :: thesis:
assume x in { w where w is Real : ( 0 <= w & w < lower_bound P ) } ; :: thesis:
then consider w0 being Real such that
A48: w0 = x and
A49: 0 <= w0 and
A50: w0 < lower_bound P ;
w0 <= 1 by A47, A50, XXREAL_0:2;
then w0 in { u where u is Real : ( 0 <= u & u <= 1 ) } by A49;
then w0 in P \/ Q by A1, BORSUK_1:40, RCOMP_1:def 1;
then ( w0 in P or w0 in Q ) by XBOOLE_0:def 3;
hence x in Q by A10, A48, A50, SEQ_4:def 2; :: thesis:

end;

then A51: { w where w is Real : ( 0 <= w & w < lower_bound P ) } c= Q ;
then reconsider D = { w where w is Real : ( 0 <= w & w < lower_bound P ) } as Subset of R^1 by A9, METRIC_1:def 13, TOPMETR:def 6, XBOOLE_1:1;
A52: not 0 in P by A6, A38, XBOOLE_0:3;

now :: thesis:

let G be Subset of R^1; :: thesis:
assume A53: G is open ; :: thesis:
assume t in G ; :: thesis:
then consider e being Real such that
A54: e > 0 and
A55: Ball (m,e) c= G by A53, TOPMETR:15, TOPMETR:def 6;
reconsider e = e as Element of REAL by XREAL_0:def 1;
reconsider e0 = max (0,((lower_bound P) - (e / 2))) as Element of REAL by XREAL_0:def 1;
reconsider e1 = e0 as Point of RealSpace by METRIC_1:def 13;
A56: e * (1 / 2) < e * 1 by A54, XREAL_1:68;
A57: real_dist . ((lower_bound P),e0) = dist (m,e1) by METRIC_1:def 1, METRIC_1:def 13;

now :: thesis:

per cases by XXREAL_0:16;

suppose A58: e0 = 0 ; :: thesis:

then lower_bound P <= e / 2 by XREAL_1:50, XXREAL_0:25;
then lower_bound P < e by A56, XXREAL_0:2;
hence |.((lower_bound P) - e0).| < e by A47, A58, ABSVALUE:def 1; :: thesis:

end;

suppose e0 = (lower_bound P) - (e / 2) ; :: thesis:

hence |.((lower_bound P) - e0).| < e by A54, A56, ABSVALUE:def 1; :: thesis:

end;

then dist (m,e1) < e by METRIC_1:def 12, A57;
then e1 in { z where z is Element of RealSpace : dist (m,z) < e } ;
then A59: e1 in Ball (m,e) by METRIC_1:17;
( e0 = 0 or e0 = (lower_bound P) - (e / 2) ) by XXREAL_0:16;
then ( 0 <= e0 & e0 < lower_bound P ) by A52, A39, A47, A54, XREAL_1:44, XREAL_1:139, XXREAL_0:25;
then e0 in { w where w is Real : ( 0 <= w & w < lower_bound P ) } ;
hence D meets G by A55, A59, XBOOLE_0:3; :: thesis:

end;

then A60: t in Cl D by PRE_TOPC:24;
A61: Cl B0 = B0 by A14, PRE_TOPC:22;
Cl D c= Cl B0 by A51, PRE_TOPC:19;
hence contradiction by A6, A39, A60, A61, XBOOLE_0:3; :: thesis:

end;

hence contradiction ; :: thesis:

end;

hence I[01] is connected by CONNSP_1:10; :: thesis: