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] and
A3: B <> {} I[01] and
A4: A is closed and
A5: B is closed ; :: thesis: A meets B
reconsider P = A, Q = B as Subset of REAL by BORSUK_1:83, XBOOLE_1:1;
assume A6: A misses B ; :: thesis: contradiction
consider x being Element of P;
reconsider x = x as Real by A2, TARSKI:def 3;
A7: now
take x = x; :: thesis: x in P
thus x in P by A2; :: thesis: verum
end;
consider x being Element of Q;
reconsider x = x as Real by A3, TARSKI:def 3;
A8: now
take x = x; :: thesis: x in Q
thus x in Q by A3; :: thesis: verum
end;
A9: the carrier of RealSpace = the carrier of (TopSpaceMetr RealSpace ) by TOPMETR:16;
now
take p = 0 ; :: thesis: for r being real number st r in P holds
p <= r
let r be real number ; :: thesis: ( r in P implies p <= r )
assume r in P ; :: thesis: p <= r
then r in [.0 ,1.] by BORSUK_1:83;
then r in { w where w is Real : ( 0 <= w & w <= 1 ) } by RCOMP_1:def 1;
then ex u being Real st
( u = r & 0 <= u & u <= 1 ) ;
hence p <= r ; :: thesis: verum
end;
then A10: P is bounded_below by SEQ_4:def 2;
now
take p = 0 ; :: thesis: for r being real number st r in Q holds
p <= r
let r be real number ; :: thesis: ( r in Q implies p <= r )
assume r in Q ; :: thesis: p <= r
then r in [.0 ,1.] by BORSUK_1:83;
then r in { w where w is Real : ( 0 <= w & w <= 1 ) } by RCOMP_1:def 1;
then ex u being Real st
( u = r & 0 <= u & u <= 1 ) ;
hence p <= r ; :: thesis: verum
end;
then A11: Q is bounded_below by SEQ_4:def 2;
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 ; :: thesis: contradiction
reconsider 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 ; :: thesis: 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; :: 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 A24: ex u0 being Real st
( u0 = lower_bound Q & 0 <= u0 & u0 <= 1 ) ;
now
let x be set ; :: thesis: ( x in { w where w is Real : ( 0 <= w & w < lower_bound Q ) } implies x in P )
assume x in { w where w is Real : ( 0 <= w & w < lower_bound Q ) } ; :: thesis: x in P
then consider w0 being Real such that
A25: w0 = x and
A26: 0 <= w0 and
A27: w0 < lower_bound Q ;
w0 <= 1 by A24, A27, XXREAL_0:2;
then w0 in { u where u is Real : ( 0 <= u & u <= 1 ) } by A26;
then w0 in P \/ Q by A1, BORSUK_1:83, RCOMP_1:def 1;
then ( w0 in P or w0 in Q ) by XBOOLE_0:def 3;
hence x in P by A11, A25, A27, SEQ_4:def 5; :: thesis: verum
end;
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 ; :: thesis: ( G is open & t in G implies D meets G )
assume A30: G is open ; :: thesis: ( t in G implies D meets G )
assume t in G ; :: thesis: D meets G
then 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;
now
per cases ( 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;
suppose max 0 ,((lower_bound Q) - (e / 2)) = (lower_bound Q) - (e / 2) ; :: thesis: abs ((lower_bound Q) - (max 0 ,((lower_bound Q) - (e / 2)))) < e
hence abs ((lower_bound Q) - (max 0 ,((lower_bound Q) - (e / 2)))) < e by A31, A33, ABSVALUE:def 1; :: thesis: verum
end;
end;
end;
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; :: thesis: 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; :: thesis: verum
end;
suppose A38: 0 in Q ; :: thesis: contradiction
reconsider 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 ; :: thesis: 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; :: 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 A46: ex u0 being Real st
( u0 = lower_bound P & 0 <= u0 & u0 <= 1 ) ;
now
let x be set ; :: thesis: ( x in { w where w is Real : ( 0 <= w & w < lower_bound P ) } implies x in Q )
assume x in { w where w is Real : ( 0 <= w & w < lower_bound P ) } ; :: thesis: x in Q
then consider w0 being Real such that
A47: w0 = x and
A48: 0 <= w0 and
A49: w0 < lower_bound P ;
w0 <= 1 by A46, A49, XXREAL_0:2;
then w0 in { u where u is Real : ( 0 <= u & u <= 1 ) } by A48;
then w0 in P \/ Q by A1, BORSUK_1:83, RCOMP_1:def 1;
then ( w0 in P or w0 in Q ) by XBOOLE_0:def 3;
hence x in Q by A10, A47, A49, SEQ_4:def 5; :: thesis: verum
end;
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 ; :: thesis: ( G is open & t in G implies D meets G )
assume A52: G is open ; :: thesis: ( t in G implies D meets G )
assume t in G ; :: thesis: D meets G
then 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;
now
per cases ( 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;
suppose max 0 ,((lower_bound P) - (e / 2)) = (lower_bound P) - (e / 2) ; :: thesis: abs ((lower_bound P) - (max 0 ,((lower_bound P) - (e / 2)))) < e
hence abs ((lower_bound P) - (max 0 ,((lower_bound P) - (e / 2)))) < e by A53, A55, ABSVALUE:def 1; :: thesis: verum
end;
end;
end;
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; :: thesis: 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; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
hence I[01] is connected by CONNSP_1:11; :: thesis: verum