let f be continuous Function of I[01],I[01]; :: thesis:
reconsider F = f as Function of [.0,1.],[.0,1.] by BORSUK_1:40;
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:
assume x in { a where a is Real : ( a in [.0,1.] & F . a in [.0,a.] ) } ; :: thesis:
then ex a being Real st
( a = x & a in [.0,1.] & F . a in [.0,a.] ) ;
hence x in REAL ; :: thesis:

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 7;
A2: A c= [.0,1.]

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A3: x in A ; :: thesis:
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:

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:
assume x in { b where b is Real : ( b in [.0,1.] & F . b in [.b,1.] ) } ; :: thesis:
then ex b being Real st
( b = x & b in [.0,1.] & F . b in [.b,1.] ) ;
hence x in REAL ; :: thesis:

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:10;
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 3;
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:
assume A10: x in [.0,1.] ; :: thesis:
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 3;

now

per cases by A11, A12, XBOOLE_0:def 3;

suppose A13: F . y in [.0,y.] ; :: thesis:

A14: A c= A \/ B by XBOOLE_1:7;
y in A by A10, A13;
hence y in A \/ B by A14; :: thesis:

end;

suppose A15: F . y in [.y,1.] ; :: thesis:

A16: B c= A \/ B by XBOOLE_1:7;
y in B by A10, A15;
hence y in A \/ B by A16; :: thesis:

end;

hence x in A \/ B ; :: thesis:

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:
assume A19: x in B ; :: thesis:
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:

end;

assume A20: for x being Point of I[01] holds f . x <> x ; :: thesis:
A21: A /\ B = {}

proof

set x = the Element of A /\ B;
assume A22: A /\ B <> {} ; :: thesis:
then A23: the Element of A /\ B in A by XBOOLE_0:def 4;
then A24: ex z being Real st
( z = the Element of A /\ B & z in [.0,1.] & F . z in [.0,z.] ) ;
reconsider x = the Element of A /\ B 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:40; :: thesis:

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 3;
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:40;
take P ; :: thesis:
take Q ; :: thesis:
thus A28: [#] I[01] = P \/ Q by A9, BORSUK_1:40, XBOOLE_0:def 10; :: thesis:
thus ( P <> {} I[01] & Q <> {} I[01] ) by A27, A7; :: thesis:
thus P is closed :: thesis:

proof

set z = the Element of (Cl P) /\ Q;
assume not P is closed ; :: thesis:
then A29: Cl P <> P by PRE_TOPC:22;
A30: (Cl P) /\ Q <> {}

proof

assume (Cl P) /\ Q = {} ; :: thesis:
then Cl P misses Q by XBOOLE_0:def 7;
then A31: Cl P c= Q ` by SUBSET_1:23;
( P c= Cl P & P = Q ` ) by A26, A28, PRE_TOPC:5, PRE_TOPC:18;
hence contradiction by A29, A31, XBOOLE_0:def 10; :: thesis:

end;

then A32: the Element of (Cl P) /\ Q in Cl P by XBOOLE_0:def 4;
A33: the Element of (Cl P) /\ Q in Q by A30, XBOOLE_0:def 4;
reconsider z = the Element of (Cl P) /\ Q 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:48;
set r = (s0 - t0) * (2 ");
reconsider m = z, n = f . z as Point of (Closed-Interval-MSpace (0,1)) by BORSUK_1:40, TOPMETR:10;
reconsider W = Ball (n,((s0 - t0) * (2 "))) as Subset of I[01] by BORSUK_1:40, TOPMETR:10;
A36: ( W is open & f is_continuous_at z ) by A1, TMAP_1:50, TOPMETR:14, TOPMETR:20;
A37: s0 - t0 <> 0 by A20;
then A38: 0 / 2 < (s0 - t0) / 2 by A35, XREAL_1:74;
then f . z in W by TBSP_1:11;
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:43;
consider s being real number such that
A41: s > 0 and
A42: Ball (m,s) c= V by A1, A39, TOPMETR:15, TOPMETR:20;
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:40, TOPMETR:10;
min (s,((s0 - t0) * (2 "))) > 0 by A38, A41, XXREAL_0:15;
then A43: z in W0 by TBSP_1:11;
set w = the Element of P /\ W0;
W0 is open by A1, TOPMETR:14, TOPMETR:20;
then P meets W0 by A32, A43, PRE_TOPC:24;
then A44: P /\ W0 <> {} I[01] by XBOOLE_0:def 7;
then A45: the Element of P /\ W0 in P by XBOOLE_0:def 4;
A46: the Element of P /\ W0 in W0 by A44, XBOOLE_0:def 4;
then reconsider w = the Element of P /\ W0 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:17;
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:4;
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:19;
A50: (s0 - t0) * (2 ") < (s0 - t0) * 1 by A35, A37, XREAL_1:68;
A51: Ball (n,((s0 - t0) * (2 "))) c= [.t0,1.]

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A52: x in Ball (n,((s0 - t0) * (2 "))) ; :: thesis:
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:17;
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:4;
then s0 - t < s0 - t0 by A53, XXREAL_0:2;
then A54: t0 <= t by XREAL_1:10;
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:

end;

A55: Ball (n,((s0 - t0) * (2 "))) c= [.d,1.]

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A56: x in Ball (n,((s0 - t0) * (2 "))) ; :: thesis:
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:17;
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 ;

suppose t <= s0 ; :: thesis:

then 0 <= s0 - t by XREAL_1:48;
then s0 - t < (s0 - t0) * (2 ") by A57, ABSVALUE:def 1;
then s0 < ((s0 - t0) * (2 ")) + t by XREAL_1:19;
then s0 - ((s0 - t0) * (2 ")) < t by XREAL_1:19;
hence d < t by A49, XXREAL_0:2; :: thesis:

end;

suppose A59: s0 < t ; :: thesis:

s0 - ((s0 - t0) * (2 ")) < s0 by A38, XREAL_1:44;
then d < s0 by A49, XXREAL_0:2;
hence d < t by A59, XXREAL_0:2; :: thesis:

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:

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:35;
then f . w1 in W by A40;
then d in B by A55, BORSUK_1:40;
hence contradiction by A26, A47, XBOOLE_0:3; :: thesis:

end;

thus Q is closed :: thesis:

proof

set z = the Element of (Cl Q) /\ P;
assume not Q is closed ; :: thesis:
then A60: Cl Q <> Q by PRE_TOPC:22;
A61: (Cl Q) /\ P <> {}

proof

assume (Cl Q) /\ P = {} ; :: thesis:
then Cl Q misses P by XBOOLE_0:def 7;
then A62: Cl Q c= P ` by SUBSET_1:23;
( Q c= Cl Q & Q = P ` ) by A26, A28, PRE_TOPC:5, PRE_TOPC:18;
hence contradiction by A60, A62, XBOOLE_0:def 10; :: thesis:

end;

then A63: the Element of (Cl Q) /\ P in Cl Q by XBOOLE_0:def 4;
A64: the Element of (Cl Q) /\ P in P by A61, XBOOLE_0:def 4;
reconsider z = the Element of (Cl Q) /\ P 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:48;
set r = (t0 - s0) * (2 ");
reconsider m = z, n = f . z as Point of (Closed-Interval-MSpace (0,1)) by BORSUK_1:40, TOPMETR:10;
reconsider W = Ball (n,((t0 - s0) * (2 "))) as Subset of I[01] by BORSUK_1:40, TOPMETR:10;
A67: ( W is open & f is_continuous_at z ) by A1, TMAP_1:50, TOPMETR:14, TOPMETR:20;
A68: t0 - s0 <> 0 by A20;
then A69: 0 / 2 < (t0 - s0) / 2 by A66, XREAL_1:74;
then f . z in W by TBSP_1:11;
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:43;
consider s being real number such that
A72: s > 0 and
A73: Ball (m,s) c= V by A1, A70, TOPMETR:15, TOPMETR:20;
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:40, TOPMETR:10;
min (s,((t0 - s0) * (2 "))) > 0 by A69, A72, XXREAL_0:15;
then A74: z in W0 by TBSP_1:11;
set w = the Element of Q /\ W0;
W0 is open by A1, TOPMETR:14, TOPMETR:20;
then Q meets W0 by A63, A74, PRE_TOPC:24;
then A75: Q /\ W0 <> {} I[01] by XBOOLE_0:def 7;
then A76: the Element of Q /\ W0 in Q by XBOOLE_0:def 4;
A77: the Element of Q /\ W0 in W0 by A75, XBOOLE_0:def 4;
then reconsider w = the Element of Q /\ W0 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:17;
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:4;
then t0 + (- d) < (t0 - s0) * (2 ") by A79, XXREAL_0:2;
then t0 < ((t0 - s0) * (2 ")) - (- d) by XREAL_1:20;
then ( s0 + ((t0 - s0) * (2 ")) = t0 - ((t0 - s0) * (2 ")) & t0 < ((t0 - s0) * (2 ")) + (- (- d)) ) ;
then A80: s0 + ((t0 - s0) * (2 ")) < d by XREAL_1:19;
A81: (t0 - s0) * (2 ") < (t0 - s0) * 1 by A66, A68, XREAL_1:68;
A82: Ball (n,((t0 - s0) * (2 "))) c= [.0,t0.]

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A83: x in Ball (n,((t0 - s0) * (2 "))) ; :: thesis:
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:17;
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:4;
then t - s0 < t0 - s0 by A84, XXREAL_0:2;
then A85: t <= t0 by XREAL_1:9;
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:

end;

A86: Ball (n,((t0 - s0) * (2 "))) c= [.0,d.]

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A87: x in Ball (n,((t0 - s0) * (2 "))) ; :: thesis:
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:17;
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 ;

suppose s0 <= t ; :: thesis:

then 0 <= t - s0 by XREAL_1:48;
then t - s0 < (t0 - s0) * (2 ") by A88, ABSVALUE:def 1;
then t < s0 + ((t0 - s0) * (2 ")) by XREAL_1:19;
hence t < d by A80, XXREAL_0:2; :: thesis:

end;

suppose A90: t < s0 ; :: thesis:

s0 < s0 + ((t0 - s0) * (2 ")) by A69, XREAL_1:29;
then s0 < d by A80, XXREAL_0:2;
hence t < d by A90, XXREAL_0:2; :: thesis:

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:

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:35;
then f . w1 in W by A71;
then d in A by A86, BORSUK_1:40;
hence contradiction by A26, A78, XBOOLE_0:3; :: thesis:

end;

thus P misses Q by A21, XBOOLE_0:def 7; :: thesis:

end;

hence contradiction by Th22, CONNSP_1:10; :: thesis: