let P7 be Subset of I[01]; ( P7 = the carrier of I[01] \ {0,1} implies ( P7 <> {} & P7 is connected ) )
assume A1:
P7 = the carrier of I[01] \ {0,1}
; ( 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
let A,
B be
Subset of
(I[01] | P7);
( [#] (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
;
A meets B
assume A10:
A misses B
;
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
then A18:
P is
bounded_below
;
0 is
LowerBound of
Q
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 TOPMETR:12, TOPMETR:def 6;
A20:
not
l in Q
proof
assume
l in Q
;
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;
verum
end;
A23:
now not l <= 0 assume A24:
l <= 0
;
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
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 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 not l5 <= r5assume A31:
l5 <= r5
;
contradictionthen
l5 = r5
by A31, XXREAL_0:1;
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;
verum end; A39:
0 < r5
by A4, A12, A25, XXREAL_1:4;
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 not l5 in Passume
l5 in P
;
contradictionthen 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;
verum end; then consider s1 being
Real such that 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;
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 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;
verum
end;
then
I[01] | P7 is connected
by CONNSP_1:11;
hence
( P7 <> {} & P7 is connected )
by A1, A2, A3, BORSUK_1:40, CONNSP_1:def 3, XBOOLE_0:def 5; verum