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 10;
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:83, 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:24;
reconsider P1 =
P7 as
Subset of
R^1 by A12, TOPMETR:24;
I[01] = R^1 | D1
by TOPMETR:26, TOPMETR:27;
then A13:
I[01] | P7 = R^1 | P1
by BORSUK_1:83, PRE_TOPC:28;
P1 = { r1 where r1 is Real : ( 0 < r1 & r1 < 1 ) }
by A12, RCOMP_1:def 2;
then
P1 is
open
by JORDAN2B:32;
then A14:
I[01] | P7 is non
empty open SubSpace of
R^1
by A1, A2, A3, A4, A13, BORSUK_1:83, 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 14, TOPMETR:16, TOPMETR:def 7;
A15:
A0 is
open
by A8, A14, TSEP_1:17;
A16:
B0 is
open
by A9, A14, TSEP_1:17;
consider xp being
Element of
P;
reconsider xp =
xp as
Real ;
A17:
xp in P
;
then A18:
P is
bounded_below
by SEQ_4:def 2;
then A19:
Q is
bounded_below
by SEQ_4:def 2;
reconsider l =
lower_bound Q as
Element of
REAL ;
reconsider m =
l as
Point of
RealSpace by METRIC_1:def 14;
reconsider t =
m as
Point of
R^1 by TOPMETR:16, TOPMETR:def 7;
A20:
not
l in Q
proof
assume
l in Q
;
contradiction
then consider s being
real number such that A21:
s > 0
and A22:
Ball m,
s c= B0
by A16, TOPMETR:22, TOPMETR:def 7;
reconsider s =
s as
Element of
REAL by XREAL_0:def 1;
reconsider e1 =
l - (s / 2) as
Point of
RealSpace by METRIC_1:def 14;
s / 2
< s
by A21, XREAL_1:218;
then
abs (l - (l - (s / 2))) < s
by A21, ABSVALUE:def 1;
then
the
distance of
RealSpace . m,
e1 < s
by METRIC_1:def 13, METRIC_1:def 14;
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:18;
then
l <= l - (s / 2)
by A19, A22, SEQ_4:def 5;
then
l + (s / 2) <= l
by XREAL_1:21;
then
(l + (s / 2)) - l <= l - l
by XREAL_1:11;
hence
contradiction
by A21, XREAL_1:141;
verum
end;
A23:
now assume A24:
l <= 0
;
contradiction
0 < xp
by A4, A12, A17, XXREAL_1:4;
then consider r5 being
real number such that A25:
r5 in Q
and A26:
r5 < l + (xp - l)
by A19, A24, SEQ_4:def 5;
reconsider r5 =
r5 as
Real by XREAL_0:def 1;
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;
A28:
xp in P5
by A26;
A29:
P5 is
bounded_below
by A18, A27, XXREAL_2:44;
reconsider l5 =
lower_bound P5 as
Real ;
reconsider m5 =
l5 as
Point of
RealSpace by METRIC_1:def 14;
A30:
now assume A31:
l5 <= r5
;
contradictionthen
l5 = r5
by A31, XXREAL_0:1;
then consider r7 being
real number such that A34:
r7 > 0
and A35:
Ball m5,
r7 c= B0
by A16, A25, TOPMETR:22, TOPMETR:def 7;
consider r9 being
real number such that A36:
r9 in P5
and A37:
r9 < l5 + r7
by A28, A29, A34, SEQ_4:def 5;
reconsider r9 =
r9 as
Real by XREAL_0:def 1;
reconsider e8 =
r9 as
Point of
RealSpace by METRIC_1:def 14;
l5 <= r9
by A29, A36, SEQ_4:def 5;
then A38:
r9 - l5 >= 0
by XREAL_1:50;
r9 - l5 < (l5 + r7) - l5
by A37, XREAL_1:11;
then
abs (r9 - l5) < r7
by A38, ABSVALUE:def 1;
then
the
distance of
RealSpace . e8,
m5 < r7
by METRIC_1:def 13, METRIC_1:def 14;
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:18;
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:52;
consider q being
Element of
P5;
A41:
q in P5
by A28;
then reconsider q1 =
q 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 5;
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 assume
l5 in P
;
contradictionthen consider s5 being
real number such that A44:
s5 > 0
and A45:
Ball m5,
s5 c= P
by A15, TOPMETR:22, TOPMETR:def 7;
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:218;
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:8;
then A49:
(((min s5,(l5 - r5)) / 2) + r5) - ((min s5,(l5 - r5)) / 2) < l5 - ((min s5,(l5 - r5)) / 2)
by XREAL_1:11;
reconsider e1 =
l5 - ((min s5,(l5 - r5)) / 2) as
Point of
RealSpace by METRIC_1:def 14;
(min s5,(l5 - r5)) / 2
< min s5,
(l5 - r5)
by A46, XREAL_1:218;
then
(min s5,(l5 - r5)) / 2
< s5
by A47, XXREAL_0:2;
then
abs (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 13;
then
dist m5,
e1 < s5
by METRIC_1:def 1, METRIC_1:def 14;
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:18;
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:31, XREAL_1:141;
then
l5 - ((min s5,(l5 - r5)) / 2) < (l5 + ((min s5,(l5 - r5)) / 2)) - ((min s5,(l5 - r5)) / 2)
by XREAL_1:11;
hence
contradiction
by A29, A50, SEQ_4:def 5;
verum end; then consider s1 being
real number such that A51:
s1 > 0
and A52:
Ball m5,
s1 c= B0
by A16, A43, TOPMETR:22, TOPMETR:def 7;
s1 / 2
> 0
by A51, XREAL_1:141;
then consider r2 being
real number such that A53:
r2 in P5
and A54:
r2 < l5 + (s1 / 2)
by A28, A29, SEQ_4:def 5;
reconsider r2 =
r2 as
Real by XREAL_0:def 1;
A55:
l5 <= r2
by A29, A53, SEQ_4:def 5;
reconsider s3 =
r2 - l5 as
Real ;
reconsider e1 =
l5 + s3 as
Point of
RealSpace by METRIC_1:def 14;
A56:
r2 - l5 >= 0
by A55, XREAL_1:50;
A57:
r2 - l5 < (l5 + (s1 / 2)) - l5
by A54, XREAL_1:16;
s1 / 2
< s1
by A51, XREAL_1:218;
then A58:
(l5 + s3) - l5 < s1
by A57, XXREAL_0:2;
abs ((l5 + s3) - l5) = (l5 + s3) - l5
by A56, ABSVALUE:def 1;
then
real_dist . (l5 + s3),
l5 < s1
by A58, METRIC_1:def 13;
then
dist e1,
m5 < s1
by METRIC_1:def 1, METRIC_1:def 14;
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:18;
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, XBOOLE_0:def 7;
verum end;
consider q being
Element of
Q;
A60:
q in Q
;
reconsider q1 =
q as
Real ;
A61:
q1 < 1
by A4, A12, A60, XXREAL_1:4;
l <= q1
by A19, SEQ_4:def 5;
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 number such that A63:
s1 > 0
and A64:
Ball m,
s1 c= A0
by A62, TOPMETR:22, TOPMETR:def 7;
s1 / 2
> 0
by A63, XREAL_1:141;
then consider r2 being
real number such that A65:
r2 in Q
and A66:
r2 < l + (s1 / 2)
by A19, SEQ_4:def 5;
reconsider r2 =
r2 as
Real by XREAL_0:def 1;
A67:
l <= r2
by A19, A65, SEQ_4:def 5;
set s3 =
r2 - l;
reconsider e1 =
l + (r2 - l) as
Point of
RealSpace by METRIC_1:def 14;
A68:
r2 - l >= 0
by A67, XREAL_1:50;
A69:
r2 - l < (l + (s1 / 2)) - l
by A66, XREAL_1:16;
s1 / 2
< s1
by A63, XREAL_1:218;
then A70:
(l + (r2 - l)) - l < s1
by A69, XXREAL_0:2;
abs ((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 13;
then
dist e1,
m < s1
by METRIC_1:def 1, METRIC_1:def 14;
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:18;
hence
contradiction
by A10, A64, A65, XBOOLE_0:3;
verum
end;
then
I[01] | P7 is connected
by CONNSP_1:12;
hence
( P7 <> {} & P7 is connected )
by A1, A2, A3, BORSUK_1:83, CONNSP_1:def 3, XBOOLE_0:def 5; verum