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] ;
( [#] I[01] = A \/ B & A <> {} I[01] & B <> {} I[01] & A is closed & B is closed implies A meets B )
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
;
A meets B
reconsider P =
A,
Q =
B as
Subset of
REAL by BORSUK_1:83, XBOOLE_1:1;
assume A6:
A misses B
;
contradiction
consider x being
Element of
P;
reconsider x =
x as
Real by A2, TARSKI:def 3;
A7:
now take x =
x;
x in Pthus
x in P
by A2;
verum end;
consider x being
Element of
Q;
reconsider x =
x as
Real by A3, TARSKI:def 3;
A8:
now take x =
x;
x in Qthus
x in Q
by A3;
verum end;
A9:
the
carrier of
RealSpace = the
carrier of
(TopSpaceMetr RealSpace )
by TOPMETR:16;
0 is
LowerBound of
P
then A10:
P is
bounded_below
by XXREAL_2:def 9;
0 is
LowerBound of
Q
then A11:
Q is
bounded_below
by XXREAL_2:def 9;
reconsider A0 =
P,
B0 =
Q as
Subset of
R^1 by METRIC_1:def 14, TOPMETR:16, TOPMETR:def 7;
A12:
I[01] is
closed SubSpace of
R^1
by Th5, TOPMETR:27;
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 per cases
( 0 in P or 0 in Q )
by A1, A15, BORSUK_1:83, XBOOLE_0:def 3;
suppose A16:
0 in P
;
contradictionreconsider B00 =
B0 ` as
Subset of
R^1 ;
set l =
lower_bound Q;
reconsider m =
lower_bound Q as
Point of
RealSpace by METRIC_1:def 14;
reconsider t =
m as
Point of
R^1 by TOPMETR:16, TOPMETR:def 7;
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
;
contradiction
then A18:
t in B00
by SUBSET_1:50;
B00 is
open
by A14, TOPS_1:29;
then consider s being
real number such that A19:
s > 0
and A20:
Ball m,
s c= B0 `
by A18, TOPMETR:22, TOPMETR:def 7;
consider r being
real number such that A21:
r in Q
and A22:
r < (lower_bound Q) + s
by A8, A11, A19, SEQ_4:def 5;
reconsider r =
r as
Real by XREAL_0:def 1;
lower_bound Q <= r
by A11, A21, SEQ_4:def 5;
then
(lower_bound Q) - r <= 0
by XREAL_1:49;
then A23:
- s < - ((lower_bound Q) - r)
by A19, XREAL_1:26;
reconsider rm =
r as
Point of
RealSpace by METRIC_1:def 14;
r - (lower_bound Q) < s
by A22, XREAL_1:21;
then
abs (r - (lower_bound Q)) < s
by A23, SEQ_2:9;
then
the
distance of
RealSpace . rm,
m < s
by METRIC_1:def 13, METRIC_1:def 14;
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:18;
hence
contradiction
by A20, A21, XBOOLE_0:def 5;
verum
end; then
lower_bound Q in [.0 ,1.]
by BORSUK_1:83;
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 )
;
then A28:
{ w where w is Real : ( 0 <= w & w < lower_bound Q ) } c= P
by TARSKI:def 3;
then reconsider D =
{ w where w is Real : ( 0 <= w & w < lower_bound Q ) } as
Subset of
R^1 by A9, METRIC_1:def 14, TOPMETR:def 7, XBOOLE_1:1;
A29:
not
0 in Q
by A6, A16, XBOOLE_0:3;
now let G be
Subset of
R^1 ;
( G is open & t in G implies D meets G )assume A30:
G is
open
;
( t in G implies D meets G )assume
t in G
;
D meets Gthen consider e being
real number such that A31:
e > 0
and A32:
Ball m,
e c= G
by A30, TOPMETR:22, TOPMETR:def 7;
reconsider e =
e as
Element of
REAL by XREAL_0:def 1;
set e0 =
max 0 ,
((lower_bound Q) - (e / 2));
reconsider e1 =
max 0 ,
((lower_bound Q) - (e / 2)) as
Point of
RealSpace by METRIC_1:def 14;
A33:
e * (1 / 2) < e * 1
by A31, XREAL_1:70;
then
the
distance of
RealSpace . m,
e1 < e
by METRIC_1:def 13, METRIC_1:def 14;
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:18;
(
max 0 ,
((lower_bound Q) - (e / 2)) = 0 or
max 0 ,
((lower_bound Q) - (e / 2)) = (lower_bound Q) - (e / 2) )
by XXREAL_0:16;
then
(
0 <= max 0 ,
((lower_bound Q) - (e / 2)) &
max 0 ,
((lower_bound Q) - (e / 2)) < lower_bound Q )
by A29, A17, A24, A31, XREAL_1:46, XREAL_1:141, XXREAL_0:25;
then
max 0 ,
((lower_bound Q) - (e / 2)) in { w where w is Real : ( 0 <= w & w < lower_bound Q ) }
;
hence
D meets G
by A32, A35, XBOOLE_0:3;
verum end; then A36:
t in Cl D
by PRE_TOPC:54;
A37:
Cl A0 = A0
by A13, PRE_TOPC:52;
Cl D c= Cl A0
by A28, PRE_TOPC:49;
hence
contradiction
by A6, A17, A36, A37, XBOOLE_0:3;
verum end; suppose A38:
0 in Q
;
contradictionreconsider A00 =
A0 ` as
Subset of
R^1 ;
set l =
lower_bound P;
reconsider m =
lower_bound P as
Point of
RealSpace by METRIC_1:def 14;
reconsider t =
m as
Point of
R^1 by TOPMETR:16, TOPMETR:def 7;
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
;
contradiction
then A40:
t in A00
by SUBSET_1:50;
A00 is
open
by A13, TOPS_1:29;
then consider s being
real number such that A41:
s > 0
and A42:
Ball m,
s c= A0 `
by A40, TOPMETR:22, TOPMETR:def 7;
consider r being
real number such that A43:
r in P
and A44:
r < (lower_bound P) + s
by A7, A10, A41, SEQ_4:def 5;
reconsider r =
r as
Real by XREAL_0:def 1;
lower_bound P <= r
by A10, A43, SEQ_4:def 5;
then
(lower_bound P) - r <= 0
by XREAL_1:49;
then A45:
- s < - ((lower_bound P) - r)
by A41, XREAL_1:26;
reconsider rm =
r as
Point of
RealSpace by METRIC_1:def 14;
r - (lower_bound P) < s
by A44, XREAL_1:21;
then
abs (r - (lower_bound P)) < s
by A45, SEQ_2:9;
then
real_dist . r,
(lower_bound P) < s
by METRIC_1:def 13;
then
dist rm,
m < s
by METRIC_1:def 1, METRIC_1:def 14;
then
rm in { q where q is Element of RealSpace : dist m,q < s }
;
then
rm in Ball m,
s
by METRIC_1:18;
hence
contradiction
by A42, A43, XBOOLE_0:def 5;
verum
end; then
lower_bound P in [.0 ,1.]
by BORSUK_1:83;
then
lower_bound P in { u where u is Real : ( 0 <= u & u <= 1 ) }
by RCOMP_1:def 1;
then A46:
ex
u0 being
Real st
(
u0 = lower_bound P &
0 <= u0 &
u0 <= 1 )
;
then A50:
{ w where w is Real : ( 0 <= w & w < lower_bound P ) } c= Q
by TARSKI:def 3;
then reconsider D =
{ w where w is Real : ( 0 <= w & w < lower_bound P ) } as
Subset of
R^1 by A9, METRIC_1:def 14, TOPMETR:def 7, XBOOLE_1:1;
A51:
not
0 in P
by A6, A38, XBOOLE_0:3;
now let G be
Subset of
R^1 ;
( G is open & t in G implies D meets G )assume A52:
G is
open
;
( t in G implies D meets G )assume
t in G
;
D meets Gthen consider e being
real number such that A53:
e > 0
and A54:
Ball m,
e c= G
by A52, TOPMETR:22, TOPMETR:def 7;
reconsider e =
e as
Real by XREAL_0:def 1;
set e0 =
max 0 ,
((lower_bound P) - (e / 2));
reconsider e1 =
max 0 ,
((lower_bound P) - (e / 2)) as
Point of
RealSpace by METRIC_1:def 14;
A55:
e * (1 / 2) < e * 1
by A53, XREAL_1:70;
then
real_dist . (lower_bound P),
(max 0 ,((lower_bound P) - (e / 2))) < e
by METRIC_1:def 13;
then
dist m,
e1 < e
by METRIC_1:def 1, METRIC_1:def 14;
then
e1 in { z where z is Element of RealSpace : dist m,z < e }
;
then A57:
e1 in Ball m,
e
by METRIC_1:18;
(
max 0 ,
((lower_bound P) - (e / 2)) = 0 or
max 0 ,
((lower_bound P) - (e / 2)) = (lower_bound P) - (e / 2) )
by XXREAL_0:16;
then
(
0 <= max 0 ,
((lower_bound P) - (e / 2)) &
max 0 ,
((lower_bound P) - (e / 2)) < lower_bound P )
by A51, A39, A46, A53, XREAL_1:46, XREAL_1:141, XXREAL_0:25;
then
max 0 ,
((lower_bound P) - (e / 2)) in { w where w is Real : ( 0 <= w & w < lower_bound P ) }
;
hence
D meets G
by A54, A57, XBOOLE_0:3;
verum end; then A58:
t in Cl D
by PRE_TOPC:54;
A59:
Cl B0 = B0
by A14, PRE_TOPC:52;
Cl D c= Cl B0
by A50, PRE_TOPC:49;
hence
contradiction
by A6, A39, A58, A59, XBOOLE_0:3;
verum end;
hence
contradiction
;
verum
end;
hence
I[01] is connected
by CONNSP_1:11; verum