let f be continuous Function of I[01] ,I[01] ; :: thesis: ex x being Point of I[01] st f . x = x
assume A1: for x being Point of I[01] holds f . x <> x ; :: thesis: contradiction
A2: Closed-Interval-TSpace 0 ,1 = TopSpaceMetr (Closed-Interval-MSpace 0 ,1) by TOPMETR:def 8;
A3: the carrier of (Closed-Interval-MSpace 0 ,1) = [.0 ,1.] by TOPMETR:14;
reconsider F = f as Function of [.0 ,1.],[.0 ,1.] by BORSUK_1:83;
A4: [.0 ,1.] = { q where q is Real : ( 0 <= q & q <= 1 ) } by RCOMP_1:def 1;
set A = { a where a is Real : ( a in [.0 ,1.] & F . a in [.0 ,a.] ) } ;
set B = { b where b is Real : ( b in [.0 ,1.] & F . b in [.b,1.] ) } ;
{ a where a is Real : ( a in [.0 ,1.] & F . a in [.0 ,a.] ) } c= REAL
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { a where a is Real : ( a in [.0 ,1.] & F . a in [.0 ,a.] ) } or x in REAL )
assume x in { a where a is Real : ( a in [.0 ,1.] & F . a in [.0 ,a.] ) } ; :: thesis: x in REAL
then ex a being Real st
( a = x & a in [.0 ,1.] & F . a in [.0 ,a.] ) ;
hence x in REAL ; :: thesis: verum
end;
then reconsider A = { a where a is Real : ( a in [.0 ,1.] & F . a in [.0 ,a.] ) } as Subset of REAL ;
{ b where b is Real : ( b in [.0 ,1.] & F . b in [.b,1.] ) } c= REAL
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { b where b is Real : ( b in [.0 ,1.] & F . b in [.b,1.] ) } or x in REAL )
assume x in { b where b is Real : ( b in [.0 ,1.] & F . b in [.b,1.] ) } ; :: thesis: x in REAL
then ex b being Real st
( b = x & b in [.0 ,1.] & F . b in [.b,1.] ) ;
hence x in REAL ; :: thesis: verum
end;
then reconsider B = { b where b is Real : ( b in [.0 ,1.] & F . b in [.b,1.] ) } as Subset of REAL ;
A5: A c= [.0 ,1.]
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in [.0 ,1.] )
assume A6: x in A ; :: thesis: x in [.0 ,1.]
then reconsider x = x as Real ;
ex a0 being Real st
( a0 = x & a0 in [.0 ,1.] & F . a0 in [.0 ,a0.] ) by A6;
hence x in [.0 ,1.] ; :: thesis: verum
end;
A7: B c= [.0 ,1.]
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in B or x in [.0 ,1.] )
assume A8: x in B ; :: thesis: x in [.0 ,1.]
then reconsider x = x as Real ;
ex b0 being Real st
( b0 = x & b0 in [.0 ,1.] & F . b0 in [.b0,1.] ) by A8;
hence x in [.0 ,1.] ; :: thesis: verum
end;
A9: [.0 ,1.] <> {} by XXREAL_1:1;
A10: A \/ B = [.0 ,1.]
proof
A11: A \/ B c= [.0 ,1.] by A5, A7, XBOOLE_1:8;
[.0 ,1.] c= A \/ B
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in [.0 ,1.] or x in A \/ B )
assume A12: x in [.0 ,1.] ; :: thesis: x in A \/ B
then reconsider y = x as Real ;
ex p being Real st
( p = y & 0 <= p & p <= 1 ) by A4, A12;
then A13: [.0 ,1.] = [.0 ,y.] \/ [.y,1.] by XXREAL_1:174;
( [.0 ,1.] = dom F & rng F c= [.0 ,1.] ) by A9, FUNCT_2:def 1;
then A14: F . y in rng F by A12, FUNCT_1:def 5;
now
per cases ( F . y in [.0 ,y.] or F . y in [.y,1.] ) by A13, A14, XBOOLE_0:def 3;
suppose F . y in [.0 ,y.] ; :: thesis: y in A \/ B
then ( y in A & A c= A \/ B ) by A12, XBOOLE_1:7;
hence y in A \/ B ; :: thesis: verum
end;
suppose F . y in [.y,1.] ; :: thesis: y in A \/ B
then ( y in B & B c= A \/ B ) by A12, XBOOLE_1:7;
hence y in A \/ B ; :: thesis: verum
end;
end;
end;
hence x in A \/ B ; :: thesis: verum
end;
hence A \/ B = [.0 ,1.] by A11, XBOOLE_0:def 10; :: thesis: verum
end;
A15: 1 in A
proof
1 in { w where w is Real : ( 0 <= w & w <= 1 ) } ;
then A16: 1 in [.0 ,1.] by RCOMP_1:def 1;
( [.0 ,1.] = dom F & rng F c= [.0 ,1.] ) by A9, FUNCT_2:def 1;
then F . 1 in rng F by A16, FUNCT_1:def 5;
hence 1 in A by A16; :: thesis: verum
end;
A17: 0 in B
proof
0 in { w where w is Real : ( 0 <= w & w <= 1 ) } ;
then A18: 0 in [.0 ,1.] by RCOMP_1:def 1;
( [.0 ,1.] = dom F & rng F c= [.0 ,1.] ) by A9, FUNCT_2:def 1;
then F . 0 in rng F by A18, FUNCT_1:def 5;
hence 0 in B by A18; :: thesis: verum
end;
A19: A /\ B = {}
proof
assume A20: A /\ B <> {} ; :: thesis: contradiction
consider x being Element of A /\ B;
A21: x in A by A20, XBOOLE_0:def 4;
then A22: ex z being Real st
( z = x & z in [.0 ,1.] & F . z in [.0 ,z.] ) ;
reconsider x = x as Real by A21;
x in B by A20, XBOOLE_0:def 4;
then ex b0 being Real st
( b0 = x & b0 in [.0 ,1.] & F . b0 in [.b0,1.] ) ;
then A23: F . x in [.0 ,x.] /\ [.x,1.] by A22, XBOOLE_0:def 4;
x in { q where q is Real : ( 0 <= q & q <= 1 ) } by A22, RCOMP_1:def 1;
then ex u being Real st
( u = x & 0 <= u & u <= 1 ) ;
then F . x in {x} by A23, XXREAL_1:418;
then F . x = x by TARSKI:def 1;
hence contradiction by A1, A22, BORSUK_1:83; :: thesis: verum
end;
then A24: A misses B by XBOOLE_0:def 7;
ex P, Q being Subset of I[01] st
( [#] I[01] = P \/ Q & P <> {} I[01] & Q <> {} I[01] & P is closed & Q is closed & P misses Q )
proof
reconsider P = A, Q = B as Subset of I[01] by A5, A7, BORSUK_1:83;
take P ; :: thesis: ex Q being Subset of I[01] st
( [#] I[01] = P \/ Q & P <> {} I[01] & Q <> {} I[01] & P is closed & Q is closed & P misses Q )
take Q ; :: thesis: ( [#] I[01] = P \/ Q & P <> {} I[01] & Q <> {} I[01] & P is closed & Q is closed & P misses Q )
thus A25: [#] I[01] = P \/ Q by A10, BORSUK_1:83; :: thesis: ( P <> {} I[01] & Q <> {} I[01] & P is closed & Q is closed & P misses Q )
thus ( P <> {} I[01] & Q <> {} I[01] ) by A15, A17; :: thesis: ( P is closed & Q is closed & P misses Q )
thus P is closed :: thesis: ( Q is closed & P misses Q )
proof
assume not P is closed ; :: thesis: contradiction
then A26: Cl P <> P by PRE_TOPC:52;
A27: (Cl P) /\ Q <> {} consider z being Element of (Cl P) /\ Q;
A29: ( z in Cl P & z in Q ) by A27, XBOOLE_0:def 4;
then reconsider z = z as Point of I[01] ;
reconsider t0 = z as Real by A29;
A30: ex c being Real st
( c = t0 & c in [.0 ,1.] & F . c in [.c,1.] ) by A29;
then reconsider s0 = F . t0 as Real ;
t0 <= s0 by A30, XXREAL_1:1;
then A31: 0 <= s0 - t0 by XREAL_1:50;
reconsider m = z, n = f . z as Point of (Closed-Interval-MSpace 0 ,1) by BORSUK_1:83, TOPMETR:14;
set r = (s0 - t0) * (2 " );
A32: s0 - t0 <> 0 by A1;
then A33: ( 0 / 2 < (s0 - t0) / 2 & 0 <> 2 ) by A31, XREAL_1:76;
A34: (s0 - t0) * (2 " ) < (s0 - t0) * 1 by A31, A32, XREAL_1:70;
A35: t0 + ((s0 - t0) * (2 " )) = s0 - ((s0 - t0) * (2 " )) ;
reconsider W = Ball n,((s0 - t0) * (2 " )) as Subset of I[01] by BORSUK_1:83, TOPMETR:14;
A36: Ball n,((s0 - t0) * (2 " )) c= [.t0,1.]
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Ball n,((s0 - t0) * (2 " )) or x in [.t0,1.] )
assume A37: x in Ball n,((s0 - t0) * (2 " )) ; :: thesis: x in [.t0,1.]
then x in [.0 ,1.] by A3;
then reconsider t = x as Real ;
reconsider u = x as Point of (Closed-Interval-MSpace 0 ,1) by A37;
Ball n,((s0 - t0) * (2 " )) = { q where q is Element of (Closed-Interval-MSpace 0 ,1) : dist n,q < (s0 - t0) * (2 " ) } by METRIC_1:18;
then ex p being Element of (Closed-Interval-MSpace 0 ,1) st
( p = u & dist n,p < (s0 - t0) * (2 " ) ) by A37;
then abs (s0 - t) < (s0 - t0) * (2 " ) by HEINE:1;
then ( abs (s0 - t) < s0 - t0 & s0 - t <= abs (s0 - t) ) by A34, ABSVALUE:11, XXREAL_0:2;
then s0 - t < s0 - t0 by XXREAL_0:2;
then A38: t0 <= t by XREAL_1:12;
t <= 1 by A3, A37, XXREAL_1:1;
then t in { q where q is Real : ( t0 <= q & q <= 1 ) } by A38;
hence x in [.t0,1.] by RCOMP_1:def 1; :: thesis: verum
end;
A39: f . z in W by A33, TBSP_1:16;
( W is open & f is_continuous_at z ) by A2, TMAP_1:55, TOPMETR:21, TOPMETR:27;
then consider V being Subset of I[01] such that
A40: V is open and
A41: z in V and
A42: f .: V c= W by A39, TMAP_1:48;
consider s being real number such that
A43: s > 0 and
A44: Ball m,s c= V by A2, A40, A41, TOPMETR:22, TOPMETR:27;
reconsider s = s as Real by XREAL_0:def 1;
set r0 = min s,((s0 - t0) * (2 " ));
A45: min s,((s0 - t0) * (2 " )) > 0 by A33, A43, XXREAL_0:15;
A46: min s,((s0 - t0) * (2 " )) <= (s0 - t0) * (2 " ) by XXREAL_0:17;
reconsider W0 = Ball m,(min s,((s0 - t0) * (2 " ))) as Subset of I[01] by BORSUK_1:83, TOPMETR:14;
A47: W0 is open by A2, TOPMETR:21, TOPMETR:27;
A48: z in W0 by A45, TBSP_1:16;
Ball m,(min s,((s0 - t0) * (2 " ))) c= Ball m,s by PCOMPS_1:1, XXREAL_0:17;
then A49: W0 c= V by A44, XBOOLE_1:1;
P meets W0 by A29, A47, A48, PRE_TOPC:54;
then A50: P /\ W0 <> {} I[01] by XBOOLE_0:def 7;
consider w being Element of P /\ W0;
A51: ( w in P & w in W0 ) by A50, XBOOLE_0:def 4;
then reconsider w = w as Point of (Closed-Interval-MSpace 0 ,1) ;
reconsider w1 = w as Point of I[01] by A51;
reconsider d = w1 as Real by A51;
Ball m,(min s,((s0 - t0) * (2 " ))) = { q where q is Element of (Closed-Interval-MSpace 0 ,1) : dist m,q < min s,((s0 - t0) * (2 " )) } by METRIC_1:18;
then ex p being Element of (Closed-Interval-MSpace 0 ,1) st
( p = w & dist m,p < min s,((s0 - t0) * (2 " )) ) by A51;
then dist w,m < (s0 - t0) * (2 " ) by A46, XXREAL_0:2;
then ( abs (d - t0) < (s0 - t0) * (2 " ) & d - t0 <= abs (d - t0) ) by ABSVALUE:11, HEINE:1;
then d - t0 < (s0 - t0) * (2 " ) by XXREAL_0:2;
then A52: d < s0 - ((s0 - t0) * (2 " )) by A35, XREAL_1:21;
A53: Ball n,((s0 - t0) * (2 " )) c= [.d,1.]
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Ball n,((s0 - t0) * (2 " )) or x in [.d,1.] )
assume A54: x in Ball n,((s0 - t0) * (2 " )) ; :: thesis: x in [.d,1.]
then A55: x in [.0 ,1.] by A3;
reconsider v = x as Point of (Closed-Interval-MSpace 0 ,1) by A54;
reconsider t = x as Real by A55;
A56: ( t0 <= t & t <= 1 ) by A36, A54, XXREAL_1:1;
Ball n,((s0 - t0) * (2 " )) = { q where q is Element of (Closed-Interval-MSpace 0 ,1) : dist n,q < (s0 - t0) * (2 " ) } by METRIC_1:18;
then ex p being Element of (Closed-Interval-MSpace 0 ,1) st
( p = v & dist n,p < (s0 - t0) * (2 " ) ) by A54;
then A57: abs (s0 - t) < (s0 - t0) * (2 " ) by HEINE:1;
now
per cases ( t <= s0 or s0 < t ) ;
suppose t <= s0 ; :: thesis: d < t
then 0 <= s0 - t by XREAL_1:50;
then s0 - t < (s0 - t0) * (2 " ) by A57, ABSVALUE:def 1;
then s0 < ((s0 - t0) * (2 " )) + t by XREAL_1:21;
then s0 - ((s0 - t0) * (2 " )) < t by XREAL_1:21;
hence d < t by A52, XXREAL_0:2; :: thesis: verum
end;
suppose A58: s0 < t ; :: thesis: d < t
s0 - ((s0 - t0) * (2 " )) < s0 by A33, XREAL_1:46;
then d < s0 by A52, XXREAL_0:2;
hence d < t by A58, XXREAL_0:2; :: thesis: verum
end;
end;
end;
then t in { w0 where w0 is Real : ( d <= w0 & w0 <= 1 ) } by A56;
hence x in [.d,1.] by RCOMP_1:def 1; :: thesis: verum
end;
F . d in [.d,1.]
proof
f . w1 in f .: V by A49, A51, FUNCT_2:43;
then f . w1 in W by A42;
hence F . d in [.d,1.] by A53; :: thesis: verum
end;
then ( d in A & d in B ) by A50, BORSUK_1:83, XBOOLE_0:def 4;
hence contradiction by A24, XBOOLE_0:3; :: thesis: verum
end;
thus Q is closed :: thesis: P misses Q
proof
assume not Q is closed ; :: thesis: contradiction
then A59: Cl Q <> Q by PRE_TOPC:52;
A60: (Cl Q) /\ P <> {} consider z being Element of (Cl Q) /\ P;
A62: ( z in Cl Q & z in P ) by A60, XBOOLE_0:def 4;
then reconsider z = z as Point of I[01] ;
reconsider t0 = z as Real by A62;
A63: ex c being Real st
( c = t0 & c in [.0 ,1.] & F . c in [.0 ,c.] ) by A62;
then reconsider s0 = F . t0 as Real ;
s0 <= t0 by A63, XXREAL_1:1;
then A64: 0 <= t0 - s0 by XREAL_1:50;
reconsider m = z, n = f . z as Point of (Closed-Interval-MSpace 0 ,1) by BORSUK_1:83, TOPMETR:14;
set r = (t0 - s0) * (2 " );
A65: t0 - s0 <> 0 by A1;
then A66: ( 0 / 2 < (t0 - s0) / 2 & 0 <> 2 ) by A64, XREAL_1:76;
A67: (t0 - s0) * (2 " ) < (t0 - s0) * 1 by A64, A65, XREAL_1:70;
A68: s0 + ((t0 - s0) * (2 " )) = t0 - ((t0 - s0) * (2 " )) ;
reconsider W = Ball n,((t0 - s0) * (2 " )) as Subset of I[01] by BORSUK_1:83, TOPMETR:14;
A69: Ball n,((t0 - s0) * (2 " )) c= [.0 ,t0.]
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Ball n,((t0 - s0) * (2 " )) or x in [.0 ,t0.] )
assume A70: x in Ball n,((t0 - s0) * (2 " )) ; :: thesis: x in [.0 ,t0.]
then x in [.0 ,1.] by A3;
then reconsider t = x as Real ;
reconsider u = x as Point of (Closed-Interval-MSpace 0 ,1) by A70;
Ball n,((t0 - s0) * (2 " )) = { q where q is Element of (Closed-Interval-MSpace 0 ,1) : dist n,q < (t0 - s0) * (2 " ) } by METRIC_1:18;
then ex p being Element of (Closed-Interval-MSpace 0 ,1) st
( p = u & dist n,p < (t0 - s0) * (2 " ) ) by A70;
then abs (t - s0) < (t0 - s0) * (2 " ) by HEINE:1;
then ( abs (t - s0) < t0 - s0 & t - s0 <= abs (t - s0) ) by A67, ABSVALUE:11, XXREAL_0:2;
then t - s0 < t0 - s0 by XXREAL_0:2;
then A71: t <= t0 by XREAL_1:11;
( 0 <= t & t <= 1 ) by A3, A70, XXREAL_1:1;
then t in { q where q is Real : ( 0 <= q & q <= t0 ) } by A71;
hence x in [.0 ,t0.] by RCOMP_1:def 1; :: thesis: verum
end;
A72: f . z in W by A66, TBSP_1:16;
( W is open & f is_continuous_at z ) by A2, TMAP_1:55, TOPMETR:21, TOPMETR:27;
then consider V being Subset of I[01] such that
A73: V is open and
A74: z in V and
A75: f .: V c= W by A72, TMAP_1:48;
consider s being real number such that
A76: s > 0 and
A77: Ball m,s c= V by A2, A73, A74, TOPMETR:22, TOPMETR:27;
reconsider s = s as Real by XREAL_0:def 1;
set r0 = min s,((t0 - s0) * (2 " ));
A78: min s,((t0 - s0) * (2 " )) > 0 by A66, A76, XXREAL_0:15;
A79: min s,((t0 - s0) * (2 " )) <= (t0 - s0) * (2 " ) by XXREAL_0:17;
reconsider W0 = Ball m,(min s,((t0 - s0) * (2 " ))) as Subset of I[01] by BORSUK_1:83, TOPMETR:14;
A80: W0 is open by A2, TOPMETR:21, TOPMETR:27;
A81: z in W0 by A78, TBSP_1:16;
Ball m,(min s,((t0 - s0) * (2 " ))) c= Ball m,s by PCOMPS_1:1, XXREAL_0:17;
then A82: W0 c= V by A77, XBOOLE_1:1;
Q meets W0 by A62, A80, A81, PRE_TOPC:54;
then A83: Q /\ W0 <> {} I[01] by XBOOLE_0:def 7;
consider w being Element of Q /\ W0;
A84: ( w in Q & w in W0 ) by A83, XBOOLE_0:def 4;
then reconsider w = w as Point of (Closed-Interval-MSpace 0 ,1) ;
reconsider w1 = w as Point of I[01] by A84;
reconsider d = w1 as Real by A84;
Ball m,(min s,((t0 - s0) * (2 " ))) = { q where q is Element of (Closed-Interval-MSpace 0 ,1) : dist m,q < min s,((t0 - s0) * (2 " )) } by METRIC_1:18;
then ex p being Element of (Closed-Interval-MSpace 0 ,1) st
( p = w & dist m,p < min s,((t0 - s0) * (2 " )) ) by A84;
then dist m,w < (t0 - s0) * (2 " ) by A79, XXREAL_0:2;
then ( abs (t0 - d) < (t0 - s0) * (2 " ) & t0 - d <= abs (t0 - d) ) by ABSVALUE:11, HEINE:1;
then t0 + (- d) < (t0 - s0) * (2 " ) by XXREAL_0:2;
then t0 < ((t0 - s0) * (2 " )) - (- d) by XREAL_1:22;
then t0 < ((t0 - s0) * (2 " )) + (- (- d)) ;
then A85: s0 + ((t0 - s0) * (2 " )) < d by A68, XREAL_1:21;
A86: Ball n,((t0 - s0) * (2 " )) c= [.0 ,d.]
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Ball n,((t0 - s0) * (2 " )) or x in [.0 ,d.] )
assume A87: x in Ball n,((t0 - s0) * (2 " )) ; :: thesis: x in [.0 ,d.]
then A88: x in [.0 ,1.] by A3;
reconsider v = x as Point of (Closed-Interval-MSpace 0 ,1) by A87;
reconsider t = x as Real by A88;
A89: ( 0 <= t & t <= t0 ) by A69, A87, XXREAL_1:1;
Ball n,((t0 - s0) * (2 " )) = { q where q is Element of (Closed-Interval-MSpace 0 ,1) : dist n,q < (t0 - s0) * (2 " ) } by METRIC_1:18;
then ex p being Element of (Closed-Interval-MSpace 0 ,1) st
( p = v & dist n,p < (t0 - s0) * (2 " ) ) by A87;
then A90: abs (t - s0) < (t0 - s0) * (2 " ) by HEINE:1;
now
per cases ( s0 <= t or t < s0 ) ;
suppose s0 <= t ; :: thesis: t < d
then 0 <= t - s0 by XREAL_1:50;
then t - s0 < (t0 - s0) * (2 " ) by A90, ABSVALUE:def 1;
then t < s0 + ((t0 - s0) * (2 " )) by XREAL_1:21;
hence t < d by A85, XXREAL_0:2; :: thesis: verum
end;
suppose A91: t < s0 ; :: thesis: t < d
s0 < s0 + ((t0 - s0) * (2 " )) by A66, XREAL_1:31;
then s0 < d by A85, XXREAL_0:2;
hence t < d by A91, XXREAL_0:2; :: thesis: verum
end;
end;
end;
then t in { w0 where w0 is Real : ( 0 <= w0 & w0 <= d ) } by A89;
hence x in [.0 ,d.] by RCOMP_1:def 1; :: thesis: verum
end;
F . d in [.0 ,d.]
proof
f . w1 in f .: V by A82, A84, FUNCT_2:43;
then f . w1 in W by A75;
hence F . d in [.0 ,d.] by A86; :: thesis: verum
end;
then ( d in A & d in B ) by A83, BORSUK_1:83, XBOOLE_0:def 4;
hence contradiction by A24, XBOOLE_0:3; :: thesis: verum
end;
thus P misses Q by A19, XBOOLE_0:def 7; :: thesis: verum
end;
hence contradiction by Th22, CONNSP_1:11; :: thesis: verum