let P7 be Subset of I[01]; :: thesis: ( P7 = the carrier of I[01] \ {0,1} implies ( P7 <> {} & P7 is connected ) )

assume A1: P7 = the carrier of I[01] \ {0,1} ; :: thesis: ( P7 <> {} & P7 is connected )

A2: 1 / 2 in [.0,1.] by XXREAL_1:1;

A3: not 1 / 2 in {0,1} by TARSKI:def 2;

A4: [#] (I[01] | P7) = P7 by PRE_TOPC:def 5;

for A, B being Subset of (I[01] | P7) st [#] (I[01] | P7) = A \/ B & A <> {} (I[01] | P7) & B <> {} (I[01] | P7) & A is open & B is open holds

A meets B

hence ( P7 <> {} & P7 is connected ) by A1, A2, A3, BORSUK_1:40, CONNSP_1:def 3, XBOOLE_0:def 5; :: thesis: verum

assume A1: P7 = the carrier of I[01] \ {0,1} ; :: thesis: ( P7 <> {} & P7 is connected )

A2: 1 / 2 in [.0,1.] by XXREAL_1:1;

A3: not 1 / 2 in {0,1} by TARSKI:def 2;

A4: [#] (I[01] | P7) = P7 by PRE_TOPC:def 5;

for A, B being Subset of (I[01] | P7) st [#] (I[01] | P7) = A \/ B & A <> {} (I[01] | P7) & B <> {} (I[01] | P7) & A is open & B is open holds

A meets B

proof

then
I[01] | P7 is connected
by CONNSP_1:11;
let A, B be Subset of (I[01] | P7); :: thesis: ( [#] (I[01] | P7) = A \/ B & A <> {} (I[01] | P7) & B <> {} (I[01] | P7) & A is open & B is open implies A meets B )

assume that

A5: [#] (I[01] | P7) = A \/ B and

A6: A <> {} (I[01] | P7) and

A7: B <> {} (I[01] | P7) and

A8: A is open and

A9: B is open ; :: thesis: A meets B

assume A10: A misses B ; :: thesis: contradiction

A11: ].0,1.[ misses {0,1} by XXREAL_1:86;

A12: P7 = (].0,1.[ \/ {0,1}) \ {0,1} by A1, BORSUK_1:40, XXREAL_1:128

.= ].0,1.[ \ {0,1} by XBOOLE_1:40

.= ].0,1.[ by A11, XBOOLE_1:83 ;

reconsider D1 = [.0,1.] as Subset of R^1 by TOPMETR:17;

reconsider P1 = P7 as Subset of R^1 by A12, TOPMETR:17;

I[01] = R^1 | D1 by TOPMETR:19, TOPMETR:20;

then A13: I[01] | P7 = R^1 | P1 by BORSUK_1:40, PRE_TOPC:7;

P1 = { r1 where r1 is Real : ( 0 < r1 & r1 < 1 ) } by A12, RCOMP_1:def 2;

then P1 is open by JORDAN2B:26;

then A14: I[01] | P7 is non empty open SubSpace of R^1 by A1, A2, A3, A4, A13, BORSUK_1:40, TSEP_1:16, XBOOLE_0:def 5;

reconsider P = A, Q = B as non empty Subset of REAL by A4, A6, A7, A12, XBOOLE_1:1;

reconsider A0 = P, B0 = Q as non empty Subset of R^1 by METRIC_1:def 13, TOPMETR:12, TOPMETR:def 6;

A15: A0 is open by A8, A14, TSEP_1:17;

A16: B0 is open by A9, A14, TSEP_1:17;

set xp = the Element of P;

reconsider xp = the Element of P as Real ;

A17: xp in P ;

0 is LowerBound of P

0 is LowerBound of Q

reconsider l = lower_bound Q as Element of REAL by XREAL_0:def 1;

reconsider m = l as Point of RealSpace by METRIC_1:def 13;

reconsider t = m as Point of R^1 by TOPMETR:12, TOPMETR:def 6;

A20: not l in Q

A60: the Element of Q in Q ;

reconsider q1 = the Element of Q as Real ;

A61: q1 < 1 by A4, A12, A60, XXREAL_1:4;

l <= q1 by A19, SEQ_4:def 2;

then l < 1 by A61, XXREAL_0:2;

then l in ].0,1.[ by A23, XXREAL_1:4;

then A62: t in A0 by A4, A5, A12, A20, XBOOLE_0:def 3;

A0 is open by A8, A14, TSEP_1:17;

then consider s1 being Real such that

A63: s1 > 0 and

A64: Ball (m,s1) c= A0 by A62, TOPMETR:15, TOPMETR:def 6;

s1 / 2 > 0 by A63, XREAL_1:139;

then consider r2 being Real such that

A65: r2 in Q and

A66: r2 < l + (s1 / 2) by A19, SEQ_4:def 2;

reconsider r2 = r2 as Element of REAL by XREAL_0:def 1;

A67: l <= r2 by A19, A65, SEQ_4:def 2;

set s3 = r2 - l;

reconsider e1 = l + (r2 - l) as Point of RealSpace by METRIC_1:def 13;

A68: r2 - l >= 0 by A67, XREAL_1:48;

A69: r2 - l < (l + (s1 / 2)) - l by A66, XREAL_1:14;

s1 / 2 < s1 by A63, XREAL_1:216;

then A70: (l + (r2 - l)) - l < s1 by A69, XXREAL_0:2;

|.((l + (r2 - l)) - l).| = (l + (r2 - l)) - l by A68, ABSVALUE:def 1;

then real_dist . ((l + (r2 - l)),l) < s1 by A70, METRIC_1:def 12;

then dist (e1,m) < s1 by METRIC_1:def 1, METRIC_1:def 13;

then l + (r2 - l) in { z where z is Element of RealSpace : dist (m,z) < s1 } ;

then l + (r2 - l) in Ball (m,s1) by METRIC_1:17;

hence contradiction by A10, A64, A65, XBOOLE_0:3; :: thesis: verum

end;assume that

A5: [#] (I[01] | P7) = A \/ B and

A6: A <> {} (I[01] | P7) and

A7: B <> {} (I[01] | P7) and

A8: A is open and

A9: B is open ; :: thesis: A meets B

assume A10: A misses B ; :: thesis: contradiction

A11: ].0,1.[ misses {0,1} by XXREAL_1:86;

A12: P7 = (].0,1.[ \/ {0,1}) \ {0,1} by A1, BORSUK_1:40, XXREAL_1:128

.= ].0,1.[ \ {0,1} by XBOOLE_1:40

.= ].0,1.[ by A11, XBOOLE_1:83 ;

reconsider D1 = [.0,1.] as Subset of R^1 by TOPMETR:17;

reconsider P1 = P7 as Subset of R^1 by A12, TOPMETR:17;

I[01] = R^1 | D1 by TOPMETR:19, TOPMETR:20;

then A13: I[01] | P7 = R^1 | P1 by BORSUK_1:40, PRE_TOPC:7;

P1 = { r1 where r1 is Real : ( 0 < r1 & r1 < 1 ) } by A12, RCOMP_1:def 2;

then P1 is open by JORDAN2B:26;

then A14: I[01] | P7 is non empty open SubSpace of R^1 by A1, A2, A3, A4, A13, BORSUK_1:40, TSEP_1:16, XBOOLE_0:def 5;

reconsider P = A, Q = B as non empty Subset of REAL by A4, A6, A7, A12, XBOOLE_1:1;

reconsider A0 = P, B0 = Q as non empty Subset of R^1 by METRIC_1:def 13, TOPMETR:12, TOPMETR:def 6;

A15: A0 is open by A8, A14, TSEP_1:17;

A16: B0 is open by A9, A14, TSEP_1:17;

set xp = the Element of P;

reconsider xp = the Element of P as Real ;

A17: xp in P ;

0 is LowerBound of P

proof

then A18:
P is bounded_below
;
let r be ExtReal; :: according to XXREAL_2:def 2 :: thesis: ( not r in P or 0 <= r )

assume r in P ; :: thesis: 0 <= r

then r in ].0,1.[ by A4, A12;

then r in { w where w is Real : ( 0 < w & w < 1 ) } by RCOMP_1:def 2;

then ex u being Real st

( u = r & 0 < u & u < 1 ) ;

hence 0 <= r ; :: thesis: verum

end;assume r in P ; :: thesis: 0 <= r

then r in ].0,1.[ by A4, A12;

then r in { w where w is Real : ( 0 < w & w < 1 ) } by RCOMP_1:def 2;

then ex u being Real st

( u = r & 0 < u & u < 1 ) ;

hence 0 <= r ; :: thesis: verum

0 is LowerBound of Q

proof

then A19:
Q is bounded_below
;
let r be ExtReal; :: according to XXREAL_2:def 2 :: thesis: ( not r in Q or 0 <= r )

assume r in Q ; :: thesis: 0 <= r

then r in ].0,1.[ by A4, A12;

then r in { w where w is Real : ( 0 < w & w < 1 ) } by RCOMP_1:def 2;

then ex u being Real st

( u = r & 0 < u & u < 1 ) ;

hence 0 <= r ; :: thesis: verum

end;assume r in Q ; :: thesis: 0 <= r

then r in ].0,1.[ by A4, A12;

then r in { w where w is Real : ( 0 < w & w < 1 ) } by RCOMP_1:def 2;

then ex u being Real st

( u = r & 0 < u & u < 1 ) ;

hence 0 <= r ; :: thesis: verum

reconsider l = lower_bound Q as Element of REAL by XREAL_0:def 1;

reconsider m = l as Point of RealSpace by METRIC_1:def 13;

reconsider t = m as Point of R^1 by TOPMETR:12, TOPMETR:def 6;

A20: not l in Q

proof

assume
l in Q
; :: thesis: contradiction

then consider s being Real such that

A21: s > 0 and

A22: Ball (m,s) c= B0 by A16, TOPMETR:15, TOPMETR:def 6;

reconsider s = s as Element of REAL by XREAL_0:def 1;

reconsider s2 = l - (s / 2) as Element of REAL by XREAL_0:def 1;

reconsider e1 = s2 as Point of RealSpace by METRIC_1:def 13;

s / 2 < s by A21, XREAL_1:216;

then |.(l - (l - (s / 2))).| < s by A21, ABSVALUE:def 1;

then the distance of RealSpace . (m,e1) < s by METRIC_1:def 12, METRIC_1:def 13;

then dist (m,e1) < s by METRIC_1:def 1;

then e1 in { z where z is Element of RealSpace : dist (m,z) < s } ;

then l - (s / 2) in Ball (m,s) by METRIC_1:17;

then l <= l - (s / 2) by A19, A22, SEQ_4:def 2;

then l + (s / 2) <= l by XREAL_1:19;

then (l + (s / 2)) - l <= l - l by XREAL_1:9;

hence contradiction by A21, XREAL_1:139; :: thesis: verum

end;then consider s being Real such that

A21: s > 0 and

A22: Ball (m,s) c= B0 by A16, TOPMETR:15, TOPMETR:def 6;

reconsider s = s as Element of REAL by XREAL_0:def 1;

reconsider s2 = l - (s / 2) as Element of REAL by XREAL_0:def 1;

reconsider e1 = s2 as Point of RealSpace by METRIC_1:def 13;

s / 2 < s by A21, XREAL_1:216;

then |.(l - (l - (s / 2))).| < s by A21, ABSVALUE:def 1;

then the distance of RealSpace . (m,e1) < s by METRIC_1:def 12, METRIC_1:def 13;

then dist (m,e1) < s by METRIC_1:def 1;

then e1 in { z where z is Element of RealSpace : dist (m,z) < s } ;

then l - (s / 2) in Ball (m,s) by METRIC_1:17;

then l <= l - (s / 2) by A19, A22, SEQ_4:def 2;

then l + (s / 2) <= l by XREAL_1:19;

then (l + (s / 2)) - l <= l - l by XREAL_1:9;

hence contradiction by A21, XREAL_1:139; :: thesis: verum

A23: now :: thesis: not l <= 0

set q = the Element of Q;assume A24:
l <= 0
; :: thesis: contradiction

0 < xp by A4, A12, A17, XXREAL_1:4;

then consider r5 being Real such that

A25: r5 in Q and

A26: r5 < l + (xp - l) by A19, A24, SEQ_4:def 2;

reconsider r5 = r5 as Real ;

A27: { s5 where s5 is Real : ( s5 in P & r5 < s5 ) } c= P

set PP5 = { s5 where s5 is Real : ( s5 in P & r5 < s5 ) } ;

A28: xp in P5 by A26;

A29: P5 is bounded_below by A18, A27, XXREAL_2:44;

reconsider l5 = lower_bound P5 as Element of REAL by XREAL_0:def 1;

reconsider m5 = l5 as Point of RealSpace by METRIC_1:def 13;

A40: l5 - r5 > 0 by A30, XREAL_1:50;

set q = the Element of P5;

A41: the Element of P5 in P5 by A28;

reconsider q1 = the Element of P5 as Real ;

q1 in P by A27, A41;

then A42: q1 < 1 by A4, A12, XXREAL_1:4;

l5 <= q1 by A28, A29, SEQ_4:def 2;

then l5 < 1 by A42, XXREAL_0:2;

then l5 in ].0,1.[ by A30, A39, XXREAL_1:4;

then A43: ( l5 in P or l5 in Q ) by A4, A5, A12, XBOOLE_0:def 3;

A51: s1 > 0 and

A52: Ball (m5,s1) c= B0 by A16, A43, TOPMETR:15, TOPMETR:def 6;

s1 / 2 > 0 by A51, XREAL_1:139;

then consider r2 being Real such that

A53: r2 in P5 and

A54: r2 < l5 + (s1 / 2) by A28, A29, SEQ_4:def 2;

reconsider r2 = r2 as Element of REAL by XREAL_0:def 1;

A55: l5 <= r2 by A29, A53, SEQ_4:def 2;

reconsider s3 = r2 - l5 as Element of REAL ;

reconsider e1 = l5 + s3 as Point of RealSpace by METRIC_1:def 13;

A56: r2 - l5 >= 0 by A55, XREAL_1:48;

A57: r2 - l5 < (l5 + (s1 / 2)) - l5 by A54, XREAL_1:14;

s1 / 2 < s1 by A51, XREAL_1:216;

then A58: (l5 + s3) - l5 < s1 by A57, XXREAL_0:2;

|.((l5 + s3) - l5).| = (l5 + s3) - l5 by A56, ABSVALUE:def 1;

then real_dist . ((l5 + s3),l5) < s1 by A58, METRIC_1:def 12;

then dist (e1,m5) < s1 by METRIC_1:def 1, METRIC_1:def 13;

then l5 + s3 in { z where z is Element of RealSpace : dist (m5,z) < s1 } ;

then l5 + s3 in Ball (m5,s1) by METRIC_1:17;

then A59: l5 + s3 in P5 /\ Q by A52, A53, XBOOLE_0:def 4;

P5 /\ Q c= P /\ Q by A27, XBOOLE_1:26;

hence contradiction by A10, A59; :: thesis: verum

end;0 < xp by A4, A12, A17, XXREAL_1:4;

then consider r5 being Real such that

A25: r5 in Q and

A26: r5 < l + (xp - l) by A19, A24, SEQ_4:def 2;

reconsider r5 = r5 as Real ;

A27: { s5 where s5 is Real : ( s5 in P & r5 < s5 ) } c= P

proof

then reconsider P5 = { s5 where s5 is Real : ( s5 in P & r5 < s5 ) } as Subset of REAL by XBOOLE_1:1;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { s5 where s5 is Real : ( s5 in P & r5 < s5 ) } or y in P )

assume y in { s5 where s5 is Real : ( s5 in P & r5 < s5 ) } ; :: thesis: y in P

then ex s5 being Real st

( s5 = y & s5 in P & r5 < s5 ) ;

hence y in P ; :: thesis: verum

end;assume y in { s5 where s5 is Real : ( s5 in P & r5 < s5 ) } ; :: thesis: y in P

then ex s5 being Real st

( s5 = y & s5 in P & r5 < s5 ) ;

hence y in P ; :: thesis: verum

set PP5 = { s5 where s5 is Real : ( s5 in P & r5 < s5 ) } ;

A28: xp in P5 by A26;

A29: P5 is bounded_below by A18, A27, XXREAL_2:44;

reconsider l5 = lower_bound P5 as Element of REAL by XREAL_0:def 1;

reconsider m5 = l5 as Point of RealSpace by METRIC_1:def 13;

A30: now :: thesis: not l5 <= r5

A39:
0 < r5
by A4, A12, A25, XXREAL_1:4;assume A31:
l5 <= r5
; :: thesis: contradiction

then consider r7 being Real such that

A34: r7 > 0 and

A35: Ball (m5,r7) c= B0 by A16, A25, TOPMETR:15, TOPMETR:def 6;

consider r9 being Real such that

A36: r9 in P5 and

A37: r9 < l5 + r7 by A28, A29, A34, SEQ_4:def 2;

reconsider r9 = r9 as Element of REAL by XREAL_0:def 1;

reconsider e8 = r9 as Point of RealSpace by METRIC_1:def 13;

l5 <= r9 by A29, A36, SEQ_4:def 2;

then A38: r9 - l5 >= 0 by XREAL_1:48;

r9 - l5 < (l5 + r7) - l5 by A37, XREAL_1:9;

then |.(r9 - l5).| < r7 by A38, ABSVALUE:def 1;

then the distance of RealSpace . (e8,m5) < r7 by METRIC_1:def 12, METRIC_1:def 13;

then dist (e8,m5) < r7 by METRIC_1:def 1;

then e8 in { z where z is Element of RealSpace : dist (m5,z) < r7 } ;

then e8 in Ball (m5,r7) by METRIC_1:17;

hence contradiction by A10, A27, A35, A36, XBOOLE_0:3; :: thesis: verum

end;now :: thesis: not l5 < r5

then
l5 = r5
by A31, XXREAL_0:1;assume
l5 < r5
; :: thesis: contradiction

then r5 - l5 > 0 by XREAL_1:50;

then consider r being Real such that

A32: r in P5 and

A33: r < l5 + (r5 - l5) by A28, A29, SEQ_4:def 2;

ex s6 being Real st

( s6 = r & s6 in P & r5 < s6 ) by A32;

hence contradiction by A33; :: thesis: verum

end;then r5 - l5 > 0 by XREAL_1:50;

then consider r being Real such that

A32: r in P5 and

A33: r < l5 + (r5 - l5) by A28, A29, SEQ_4:def 2;

ex s6 being Real st

( s6 = r & s6 in P & r5 < s6 ) by A32;

hence contradiction by A33; :: thesis: verum

then consider r7 being Real such that

A34: r7 > 0 and

A35: Ball (m5,r7) c= B0 by A16, A25, TOPMETR:15, TOPMETR:def 6;

consider r9 being Real such that

A36: r9 in P5 and

A37: r9 < l5 + r7 by A28, A29, A34, SEQ_4:def 2;

reconsider r9 = r9 as Element of REAL by XREAL_0:def 1;

reconsider e8 = r9 as Point of RealSpace by METRIC_1:def 13;

l5 <= r9 by A29, A36, SEQ_4:def 2;

then A38: r9 - l5 >= 0 by XREAL_1:48;

r9 - l5 < (l5 + r7) - l5 by A37, XREAL_1:9;

then |.(r9 - l5).| < r7 by A38, ABSVALUE:def 1;

then the distance of RealSpace . (e8,m5) < r7 by METRIC_1:def 12, METRIC_1:def 13;

then dist (e8,m5) < r7 by METRIC_1:def 1;

then e8 in { z where z is Element of RealSpace : dist (m5,z) < r7 } ;

then e8 in Ball (m5,r7) by METRIC_1:17;

hence contradiction by A10, A27, A35, A36, XBOOLE_0:3; :: thesis: verum

A40: l5 - r5 > 0 by A30, XREAL_1:50;

set q = the Element of P5;

A41: the Element of P5 in P5 by A28;

reconsider q1 = the Element of P5 as Real ;

q1 in P by A27, A41;

then A42: q1 < 1 by A4, A12, XXREAL_1:4;

l5 <= q1 by A28, A29, SEQ_4:def 2;

then l5 < 1 by A42, XXREAL_0:2;

then l5 in ].0,1.[ by A30, A39, XXREAL_1:4;

then A43: ( l5 in P or l5 in Q ) by A4, A5, A12, XBOOLE_0:def 3;

now :: thesis: not l5 in P

then consider s1 being Real such that assume
l5 in P
; :: thesis: contradiction

then consider s5 being Real such that

A44: s5 > 0 and

A45: Ball (m5,s5) c= P by A15, TOPMETR:15, TOPMETR:def 6;

reconsider s5 = s5 as Element of REAL by XREAL_0:def 1;

set s59 = min (s5,(l5 - r5));

A46: min (s5,(l5 - r5)) > 0 by A40, A44, XXREAL_0:21;

A47: min (s5,(l5 - r5)) <= s5 by XXREAL_0:17;

A48: (min (s5,(l5 - r5))) / 2 < min (s5,(l5 - r5)) by A46, XREAL_1:216;

min (s5,(l5 - r5)) <= l5 - r5 by XXREAL_0:17;

then (min (s5,(l5 - r5))) / 2 < l5 - r5 by A48, XXREAL_0:2;

then ((min (s5,(l5 - r5))) / 2) + r5 < (l5 - r5) + r5 by XREAL_1:6;

then A49: (((min (s5,(l5 - r5))) / 2) + r5) - ((min (s5,(l5 - r5))) / 2) < l5 - ((min (s5,(l5 - r5))) / 2) by XREAL_1:9;

reconsider e1 = l5 - ((min (s5,(l5 - r5))) / 2) as Element of REAL by XREAL_0:def 1;

reconsider e1 = e1 as Point of RealSpace by METRIC_1:def 13;

(min (s5,(l5 - r5))) / 2 < min (s5,(l5 - r5)) by A46, XREAL_1:216;

then (min (s5,(l5 - r5))) / 2 < s5 by A47, XXREAL_0:2;

then |.(l5 - (l5 - ((min (s5,(l5 - r5))) / 2))).| < s5 by A46, ABSVALUE:def 1;

then real_dist . (l5,(l5 - ((min (s5,(l5 - r5))) / 2))) < s5 by METRIC_1:def 12;

then dist (m5,e1) < s5 by METRIC_1:def 1, METRIC_1:def 13;

then e1 in { z where z is Element of RealSpace : dist (m5,z) < s5 } ;

then l5 - ((min (s5,(l5 - r5))) / 2) in Ball (m5,s5) by METRIC_1:17;

then A50: l5 - ((min (s5,(l5 - r5))) / 2) in { s7 where s7 is Real : ( s7 in P & r5 < s7 ) } by A45, A49;

l5 < l5 + ((min (s5,(l5 - r5))) / 2) by A46, XREAL_1:29, XREAL_1:139;

then l5 - ((min (s5,(l5 - r5))) / 2) < (l5 + ((min (s5,(l5 - r5))) / 2)) - ((min (s5,(l5 - r5))) / 2) by XREAL_1:9;

hence contradiction by A29, A50, SEQ_4:def 2; :: thesis: verum

end;then consider s5 being Real such that

A44: s5 > 0 and

A45: Ball (m5,s5) c= P by A15, TOPMETR:15, TOPMETR:def 6;

reconsider s5 = s5 as Element of REAL by XREAL_0:def 1;

set s59 = min (s5,(l5 - r5));

A46: min (s5,(l5 - r5)) > 0 by A40, A44, XXREAL_0:21;

A47: min (s5,(l5 - r5)) <= s5 by XXREAL_0:17;

A48: (min (s5,(l5 - r5))) / 2 < min (s5,(l5 - r5)) by A46, XREAL_1:216;

min (s5,(l5 - r5)) <= l5 - r5 by XXREAL_0:17;

then (min (s5,(l5 - r5))) / 2 < l5 - r5 by A48, XXREAL_0:2;

then ((min (s5,(l5 - r5))) / 2) + r5 < (l5 - r5) + r5 by XREAL_1:6;

then A49: (((min (s5,(l5 - r5))) / 2) + r5) - ((min (s5,(l5 - r5))) / 2) < l5 - ((min (s5,(l5 - r5))) / 2) by XREAL_1:9;

reconsider e1 = l5 - ((min (s5,(l5 - r5))) / 2) as Element of REAL by XREAL_0:def 1;

reconsider e1 = e1 as Point of RealSpace by METRIC_1:def 13;

(min (s5,(l5 - r5))) / 2 < min (s5,(l5 - r5)) by A46, XREAL_1:216;

then (min (s5,(l5 - r5))) / 2 < s5 by A47, XXREAL_0:2;

then |.(l5 - (l5 - ((min (s5,(l5 - r5))) / 2))).| < s5 by A46, ABSVALUE:def 1;

then real_dist . (l5,(l5 - ((min (s5,(l5 - r5))) / 2))) < s5 by METRIC_1:def 12;

then dist (m5,e1) < s5 by METRIC_1:def 1, METRIC_1:def 13;

then e1 in { z where z is Element of RealSpace : dist (m5,z) < s5 } ;

then l5 - ((min (s5,(l5 - r5))) / 2) in Ball (m5,s5) by METRIC_1:17;

then A50: l5 - ((min (s5,(l5 - r5))) / 2) in { s7 where s7 is Real : ( s7 in P & r5 < s7 ) } by A45, A49;

l5 < l5 + ((min (s5,(l5 - r5))) / 2) by A46, XREAL_1:29, XREAL_1:139;

then l5 - ((min (s5,(l5 - r5))) / 2) < (l5 + ((min (s5,(l5 - r5))) / 2)) - ((min (s5,(l5 - r5))) / 2) by XREAL_1:9;

hence contradiction by A29, A50, SEQ_4:def 2; :: thesis: verum

A51: s1 > 0 and

A52: Ball (m5,s1) c= B0 by A16, A43, TOPMETR:15, TOPMETR:def 6;

s1 / 2 > 0 by A51, XREAL_1:139;

then consider r2 being Real such that

A53: r2 in P5 and

A54: r2 < l5 + (s1 / 2) by A28, A29, SEQ_4:def 2;

reconsider r2 = r2 as Element of REAL by XREAL_0:def 1;

A55: l5 <= r2 by A29, A53, SEQ_4:def 2;

reconsider s3 = r2 - l5 as Element of REAL ;

reconsider e1 = l5 + s3 as Point of RealSpace by METRIC_1:def 13;

A56: r2 - l5 >= 0 by A55, XREAL_1:48;

A57: r2 - l5 < (l5 + (s1 / 2)) - l5 by A54, XREAL_1:14;

s1 / 2 < s1 by A51, XREAL_1:216;

then A58: (l5 + s3) - l5 < s1 by A57, XXREAL_0:2;

|.((l5 + s3) - l5).| = (l5 + s3) - l5 by A56, ABSVALUE:def 1;

then real_dist . ((l5 + s3),l5) < s1 by A58, METRIC_1:def 12;

then dist (e1,m5) < s1 by METRIC_1:def 1, METRIC_1:def 13;

then l5 + s3 in { z where z is Element of RealSpace : dist (m5,z) < s1 } ;

then l5 + s3 in Ball (m5,s1) by METRIC_1:17;

then A59: l5 + s3 in P5 /\ Q by A52, A53, XBOOLE_0:def 4;

P5 /\ Q c= P /\ Q by A27, XBOOLE_1:26;

hence contradiction by A10, A59; :: thesis: verum

A60: the Element of Q in Q ;

reconsider q1 = the Element of Q as Real ;

A61: q1 < 1 by A4, A12, A60, XXREAL_1:4;

l <= q1 by A19, SEQ_4:def 2;

then l < 1 by A61, XXREAL_0:2;

then l in ].0,1.[ by A23, XXREAL_1:4;

then A62: t in A0 by A4, A5, A12, A20, XBOOLE_0:def 3;

A0 is open by A8, A14, TSEP_1:17;

then consider s1 being Real such that

A63: s1 > 0 and

A64: Ball (m,s1) c= A0 by A62, TOPMETR:15, TOPMETR:def 6;

s1 / 2 > 0 by A63, XREAL_1:139;

then consider r2 being Real such that

A65: r2 in Q and

A66: r2 < l + (s1 / 2) by A19, SEQ_4:def 2;

reconsider r2 = r2 as Element of REAL by XREAL_0:def 1;

A67: l <= r2 by A19, A65, SEQ_4:def 2;

set s3 = r2 - l;

reconsider e1 = l + (r2 - l) as Point of RealSpace by METRIC_1:def 13;

A68: r2 - l >= 0 by A67, XREAL_1:48;

A69: r2 - l < (l + (s1 / 2)) - l by A66, XREAL_1:14;

s1 / 2 < s1 by A63, XREAL_1:216;

then A70: (l + (r2 - l)) - l < s1 by A69, XXREAL_0:2;

|.((l + (r2 - l)) - l).| = (l + (r2 - l)) - l by A68, ABSVALUE:def 1;

then real_dist . ((l + (r2 - l)),l) < s1 by A70, METRIC_1:def 12;

then dist (e1,m) < s1 by METRIC_1:def 1, METRIC_1:def 13;

then l + (r2 - l) in { z where z is Element of RealSpace : dist (m,z) < s1 } ;

then l + (r2 - l) in Ball (m,s1) by METRIC_1:17;

hence contradiction by A10, A64, A65, XBOOLE_0:3; :: thesis: verum

hence ( P7 <> {} & P7 is connected ) by A1, A2, A3, BORSUK_1:40, CONNSP_1:def 3, XBOOLE_0:def 5; :: thesis: verum