let P7 be Subset of I; :: thesis: ( P7 = the carrier of I \ {0,1} implies ( P7 <> {} & P7 is connected ) )
assume A1: P7 = the carrier of I \ {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 | P7) = P7 by PRE_TOPC:def 5;
for A, B being Subset of (I | P7) st [#] (I | P7) = A \/ B & A <> {} (I | P7) & B <> {} (I | P7) & A is open & B is open holds
A meets B
proof
let A, B be Subset of (I | P7); :: thesis: ( [#] (I | P7) = A \/ B & A <> {} (I | P7) & B <> {} (I | P7) & A is open & B is open implies A meets B )
assume that
A5: [#] (I | P7) = A \/ B and
A6: A <> {} (I | P7) and
A7: B <> {} (I | 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
.= ].0,1.[ \ {0,1} by XBOOLE_1:40
.= ].0,1.[ by ;
reconsider D1 = [.0,1.] as Subset of R^1 by TOPMETR:17;
reconsider P1 = P7 as Subset of R^1 by ;
I = R^1 | D1 by ;
then A13: I | P7 = R^1 | P1 by ;
P1 = { r1 where r1 is Real : ( 0 < r1 & r1 < 1 ) } by ;
then P1 is open by JORDAN2B:26;
then A14: I | P7 is non empty open SubSpace of R^1 by ;
reconsider P = A, Q = B as non empty Subset of REAL by ;
reconsider A0 = P, B0 = Q as non empty Subset of R^1 by ;
A15: A0 is open by ;
A16: B0 is open by ;
set xp = the Element of P;
reconsider xp = the Element of P as Real ;
A17: xp in P ;
0 is LowerBound of P
proof
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 ;
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;
then A18: P is bounded_below ;
0 is LowerBound of Q
proof
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 ;
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;
then A19: Q is bounded_below ;
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 ;
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 ;
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 ;
then |.(l - (l - (s / 2))).| < s by ;
then the distance of RealSpace . (m,e1) < s by ;
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 ;
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;
A23: now :: thesis: not l <= 0
assume A24: l <= 0 ; :: thesis: contradiction
0 < xp by ;
then consider r5 being Real such that
A25: r5 in Q and
A26: r5 < l + (xp - l) by ;
reconsider r5 = r5 as Real ;
A27: { s5 where s5 is Real : ( s5 in P & r5 < s5 ) } c= P
proof
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;
then reconsider P5 = { s5 where s5 is Real : ( s5 in P & r5 < s5 ) } as Subset of REAL by XBOOLE_1:1;
set PP5 = { s5 where s5 is Real : ( s5 in P & r5 < s5 ) } ;
A28: xp in P5 by A26;
A29: P5 is bounded_below by ;
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
assume A31: l5 <= r5 ; :: thesis: contradiction
now :: thesis: not l5 < r5
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 ;
ex s6 being Real st
( s6 = r & s6 in P & r5 < s6 ) by A32;
hence contradiction by A33; :: thesis: verum
end;
then l5 = r5 by ;
then consider r7 being Real such that
A34: r7 > 0 and
A35: Ball (m5,r7) c= B0 by ;
consider r9 being Real such that
A36: r9 in P5 and
A37: r9 < l5 + r7 by ;
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 ;
then A38: r9 - l5 >= 0 by XREAL_1:48;
r9 - l5 < (l5 + r7) - l5 by ;
then |.(r9 - l5).| < r7 by ;
then the distance of RealSpace . (e8,m5) < r7 by ;
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;
A39: 0 < r5 by ;
A40: l5 - r5 > 0 by ;
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 ;
then A42: q1 < 1 by ;
l5 <= q1 by ;
then l5 < 1 by ;
then l5 in ].0,1.[ by ;
then A43: ( l5 in P or l5 in Q ) by ;
now :: thesis: not l5 in P
assume l5 in P ; :: thesis: contradiction
then consider s5 being Real such that
A44: s5 > 0 and
A45: Ball (m5,s5) c= P by ;
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 ;
A47: min (s5,(l5 - r5)) <= s5 by XXREAL_0:17;
A48: (min (s5,(l5 - r5))) / 2 < min (s5,(l5 - r5)) by ;
min (s5,(l5 - r5)) <= l5 - r5 by XXREAL_0:17;
then (min (s5,(l5 - r5))) / 2 < l5 - r5 by ;
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 ;
then (min (s5,(l5 - r5))) / 2 < s5 by ;
then |.(l5 - (l5 - ((min (s5,(l5 - r5))) / 2))).| < s5 by ;
then real_dist . (l5,(l5 - ((min (s5,(l5 - r5))) / 2))) < s5 by METRIC_1:def 12;
then dist (m5,e1) < s5 by ;
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 ;
l5 < l5 + ((min (s5,(l5 - r5))) / 2) by ;
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 s1 being Real such that
A51: s1 > 0 and
A52: Ball (m5,s1) c= B0 by ;
s1 / 2 > 0 by ;
then consider r2 being Real such that
A53: r2 in P5 and
A54: r2 < l5 + (s1 / 2) by ;
reconsider r2 = r2 as Element of REAL by XREAL_0:def 1;
A55: l5 <= r2 by ;
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 ;
A57: r2 - l5 < (l5 + (s1 / 2)) - l5 by ;
s1 / 2 < s1 by ;
then A58: (l5 + s3) - l5 < s1 by ;
|.((l5 + s3) - l5).| = (l5 + s3) - l5 by ;
then real_dist . ((l5 + s3),l5) < s1 by ;
then dist (e1,m5) < s1 by ;
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 ;
P5 /\ Q c= P /\ Q by ;
hence contradiction by A10, A59; :: thesis: verum
end;
set q = the Element of Q;
A60: the Element of Q in Q ;
reconsider q1 = the Element of Q as Real ;
A61: q1 < 1 by ;
l <= q1 by ;
then l < 1 by ;
then l in ].0,1.[ by ;
then A62: t in A0 by ;
A0 is open by ;
then consider s1 being Real such that
A63: s1 > 0 and
A64: Ball (m,s1) c= A0 by ;
s1 / 2 > 0 by ;
then consider r2 being Real such that
A65: r2 in Q and
A66: r2 < l + (s1 / 2) by ;
reconsider r2 = r2 as Element of REAL by XREAL_0:def 1;
A67: l <= r2 by ;
set s3 = r2 - l;
reconsider e1 = l + (r2 - l) as Point of RealSpace by METRIC_1:def 13;
A68: r2 - l >= 0 by ;
A69: r2 - l < (l + (s1 / 2)) - l by ;
s1 / 2 < s1 by ;
then A70: (l + (r2 - l)) - l < s1 by ;
|.((l + (r2 - l)) - l).| = (l + (r2 - l)) - l by ;
then real_dist . ((l + (r2 - l)),l) < s1 by ;
then dist (e1,m) < s1 by ;
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;
then I | P7 is connected by CONNSP_1:11;
hence ( P7 <> {} & P7 is connected ) by ; :: thesis: verum