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