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