let n be Nat; :: thesis: for F being Function of [:(TOP-REAL n),I[01]:],(TOP-REAL n) st ( for x being Point of (TOP-REAL n)
for i being Point of I[01] holds F . (x,i) = (1 - i) * x ) holds
F is continuous
set I = the carrier of I[01];
let F be Function of [:(TOP-REAL n),I[01]:],(TOP-REAL n); :: thesis: ( ( for x being Point of (TOP-REAL n)
for i being Point of I[01] holds F . (x,i) = (1 - i) * x ) implies F is continuous )
assume A1: for x being Point of (TOP-REAL n)
for i being Point of I[01] holds F . (x,i) = (1 - i) * x ; :: thesis: F is continuous
A2: REAL n = n -tuples_on REAL by EUCLID:def 1;
A3: [#] I[01] = the carrier of I[01] ;
for p being Point of [:(TOP-REAL n),I[01]:]
for V being Subset of (TOP-REAL n) st F . p in V & V is open holds
ex W being Subset of [:(TOP-REAL n),I[01]:] st
( p in W & W is open & F .: W c= V )

proof

let p be Point of [:(TOP-REAL n),I[01]:]; :: thesis: for V being Subset of (TOP-REAL n) st F . p in V & V is open holds
ex W being Subset of [:(TOP-REAL n),I[01]:] st
( p in W & W is open & F .: W c= V )
let V be Subset of (TOP-REAL n); :: thesis: ( F . p in V & V is open implies ex W being Subset of [:(TOP-REAL n),I[01]:] st
( p in W & W is open & F .: W c= V ) )
reconsider ep = F . p as Point of (Euclid n) by TOPREAL3:8;
consider x being Point of (TOP-REAL n), i being Point of I[01] such that
A4: p = [x,i] by BORSUK_1:10;
A5: ep = F . (x,i) by A4
.= (1 - i) * x by A1 ;
reconsider fx = x as Element of REAL n by EUCLID:22;
reconsider lx = x as Point of (Euclid n) by TOPREAL3:8;
A6: n in NAT by ORDINAL1:def 12;
assume ( F . p in V & V is open ) ; :: thesis: ex W being Subset of [:(TOP-REAL n),I[01]:] st
( p in W & W is open & F .: W c= V )
then F . p in Int V by TOPS_1:23;
then consider r0 being real number such that
A7: r0 > 0 and
A8: Ball (ep,r0) c= V by A6, GOBOARD6:5;
A9: r0 / 2 > 0 by A7, XREAL_1:139;

per cases ( 1 - i > 0 or 1 - i <= 0 ) ;

suppose A10: 1 - i > 0 ; :: thesis: ex W being Subset of [:(TOP-REAL n),I[01]:] st
( p in W & W is open & F .: W c= V )

then - (- (1 - i)) > - 0 ;
then - (1 - i) < 0 ;
then A11: (i - 1) * ((2 * (1 - i)) * |.fx.|) <= 0 by A10;
set t = ((2 * (1 - i)) * |.fx.|) + r0;
set c = ((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0);
i + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0)) = ((i * (((2 * (1 - i)) * |.fx.|) + r0)) / (((2 * (1 - i)) * |.fx.|) + r0)) + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0)) by A7, A10, XCMPLX_1:89
.= ((i * (((2 * (1 - i)) * |.fx.|) + r0)) + ((1 - i) * r0)) / (((2 * (1 - i)) * |.fx.|) + r0) by XCMPLX_1:62
.= ((((i * 2) * (1 - i)) * |.fx.|) + r0) / (((2 * (1 - i)) * |.fx.|) + r0) ;
then (i + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))) - 1 = (((((i * 2) * (1 - i)) * |.fx.|) + r0) / (((2 * (1 - i)) * |.fx.|) + r0)) - ((((2 * (1 - i)) * |.fx.|) + r0) / (((2 * (1 - i)) * |.fx.|) + r0)) by A7, A10, XCMPLX_1:60
.= (((((i * 2) * (1 - i)) * |.fx.|) + r0) - (((2 * (1 - i)) * |.fx.|) + r0)) / (((2 * (1 - i)) * |.fx.|) + r0) by XCMPLX_1:120 ;
then A12: ((i + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))) - 1) + 1 <= 0 + 1 by A7, A10, A11, XREAL_1:7;
set X1 = ].(i - (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))),(i + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))).[;
set X2 = ].(i - (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))),(i + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))).[ /\ the carrier of I[01];
reconsider X2 = ].(i - (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))),(i + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))).[ /\ the carrier of I[01] as Subset of I[01] by XBOOLE_1:17;
reconsider B = Ball (lx,((r0 / 2) / (1 - i))) as Subset of (TOP-REAL n) by TOPREAL3:8;
take W = [:B,X2:]; :: thesis: ( p in W & W is open & F .: W c= V )
0 < (1 - i) * r0 by A7, A10, XREAL_1:129;
then A13: 0 < ((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0) by A7, A10, XREAL_1:139;
then abs (i - i) < ((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0) by ABSVALUE:def 1;
then i in ].(i - (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))),(i + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))).[ by RCOMP_1:1;
then A14: i in X2 by XBOOLE_0:def 4;
0 <= i by BORSUK_1:43;
then A15: i + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0)) is Point of I[01] by A7, A10, A12, BORSUK_1:43;

A16: now

per cases ( 0 <= i - (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0)) or i - (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0)) < 0 ) ;

suppose A17: 0 <= i - (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0)) ; :: thesis: X2 is open

].(i - (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))),(i + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))).[ c= the carrier of I[01]

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in ].(i - (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))),(i + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))).[ or a in the carrier of I[01] )
assume A18: a in ].(i - (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))),(i + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))).[ ; :: thesis: a in the carrier of I[01]
then reconsider a = a as Real ;
a < i + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0)) by A18, XXREAL_1:4;
then A19: a < 1 by A12, XXREAL_0:2;
0 < a by A17, A18, XXREAL_1:4;
hence a in the carrier of I[01] by A19, BORSUK_1:43; :: thesis: verum

end;

then reconsider X1 = ].(i - (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))),(i + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))).[ as Subset of I[01] ;

now

per cases ( i - (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0)) <= i + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0)) or i - (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0)) > i + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0)) ) ;

suppose i - (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0)) <= i + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0)) ; :: thesis: X1 is open

then i - (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0)) <= 1 by A12, XXREAL_0:2;
then i - (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0)) is Point of I[01] by A17, BORSUK_1:43;
hence X1 is open by A15, BORSUK_4:45; :: thesis: verum

end;

suppose i - (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0)) > i + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0)) ; :: thesis: X1 is open

then X1 = {} I[01] by XXREAL_1:28;
hence X1 is open ; :: thesis: verum

end;

end;

end;

hence X2 is open by A3; :: thesis: verum

end;

suppose A20: i - (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0)) < 0 ; :: thesis: X2 is open

X2 = [.0,(i + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))).[

proof

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: [.0,(i + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))).[ c= X2

let a be set ; :: thesis: ( a in X2 implies a in [.0,(i + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))).[ )
assume A21: a in X2 ; :: thesis: a in [.0,(i + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))).[
then reconsider b = a as Real ;
a in ].(i - (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))),(i + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))).[ by A21, XBOOLE_0:def 4;
then A22: b < i + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0)) by XXREAL_1:4;
0 <= b by A21, BORSUK_1:43;
hence a in [.0,(i + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))).[ by A22, XXREAL_1:3; :: thesis: verum

end;

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in [.0,(i + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))).[ or a in X2 )
assume A23: a in [.0,(i + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))).[ ; :: thesis: a in X2
then reconsider b = a as Real ;
A24: 0 <= b by A23, XXREAL_1:3;
A25: b < i + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0)) by A23, XXREAL_1:3;
then b <= 1 by A12, XXREAL_0:2;
then A26: a in the carrier of I[01] by A24, BORSUK_1:40, XXREAL_1:1;
a in ].(i - (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))),(i + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))).[ by A20, A25, A24, XXREAL_1:4;
hence a in X2 by A26, XBOOLE_0:def 4; :: thesis: verum

end;

hence X2 is open by A15, Th5; :: thesis: verum

end;

end;

end;

x in B by A9, A10, GOBOARD6:1, XREAL_1:139;
hence p in W by A4, A14, ZFMISC_1:87; :: thesis: ( W is open & F .: W c= V )
B is open by A6, GOBOARD6:3;
hence W is open by A16, BORSUK_1:6; :: thesis: F .: W c= V
A27: 0 < 2 * (1 - i) by A10, XREAL_1:129;
F .: W c= Ball (ep,r0)

proof

let m be set ; :: according to TARSKI:def 3 :: thesis: ( not m in F .: W or m in Ball (ep,r0) )
assume m in F .: W ; :: thesis: m in Ball (ep,r0)
then consider z being set such that
A28: z in dom F and
A29: z in W and
A30: F . z = m by FUNCT_1:def 6;
reconsider z = z as Point of [:(TOP-REAL n),I[01]:] by A28;
consider y being Point of (TOP-REAL n), j being Point of I[01] such that
A31: z = [y,j] by BORSUK_1:10;
reconsider ez = F . z, ey = y as Point of (Euclid n) by TOPREAL3:8;
reconsider fp = ep, fz = ez, fe = (1 - i) * y, fy = y as Element of REAL n by EUCLID:22;
A32: ( (1 - i) * ((r0 / (1 - i)) / 2) = r0 / 2 & (r0 / 2) / (1 - i) = (r0 / (1 - i)) / 2 ) by A10, XCMPLX_1:48, XCMPLX_1:97;
fy in B by A29, A31, ZFMISC_1:87;
then A33: dist (lx,ey) < (r0 / 2) / (1 - i) by METRIC_1:11;
j in X2 by A29, A31, ZFMISC_1:87;
then j in ].(i - (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))),(i + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))).[ by XBOOLE_0:def 4;
then abs (j - i) < ((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0) by RCOMP_1:1;
then abs (i - j) < ((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0) by UNIFORM1:11;
then A34: (abs (i - j)) * |.fy.| <= (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0)) * |.fy.| by XREAL_1:64;
reconsider yy = ey as Element of n -tuples_on REAL by A2, EUCLID:22;
A35: fe = (1 - i) * yy by EUCLID:65;
ez = F . (y,j) by A31
.= (1 - j) * y by A1 ;
then fe - fz = ((1 - i) * yy) - ((1 - j) * yy) by A35, EUCLID:65;
then A36: |.(fe - fz).| = |.(((1 - i) - (1 - j)) * fy).| by Th8
.= (abs (j - i)) * |.fy.| by EUCLID:11
.= (abs (i - j)) * |.fy.| by UNIFORM1:11 ;
reconsider gx = fx, gy = fy as Element of n -tuples_on REAL by EUCLID:def 1;
A37: ( dist (ep,ez) = |.(fp - fz).| & |.(fp - fz).| <= |.(fp - fe).| + |.(fe - fz).| ) by A6, EUCLID:19, SPPOL_1:5;
A38: (1 - i) * (fx - fy) = (1 - i) * (gx - gy)
.= ((1 - i) * gx) - ((1 - i) * gy) by Th7
.= ((1 - i) * fx) - ((1 - i) * fy)
.= ((1 - i) * fx) - fe by EUCLID:65 ;
A39: dist (lx,ey) = |.(fx - fy).| by A6, SPPOL_1:5;
then (1 - i) * |.(fx - fy).| < (1 - i) * ((r0 / 2) / (1 - i)) by A10, A33, XREAL_1:68;
then (abs (1 - i)) * |.(fx - fy).| < r0 / 2 by A10, A32, ABSVALUE:def 1;
then A40: |.(((1 - i) * fx) - fe).| < r0 / 2 by A38, EUCLID:11;
( |.(fx - fy).| = |.(fy - fx).| & |.fy.| - |.fx.| <= |.(fy - fx).| ) by EUCLID:15, EUCLID:18;
then |.fy.| - |.fx.| < (r0 / 2) / (1 - i) by A33, A39, XXREAL_0:2;
then |.fy.| < |.fx.| + ((r0 / 2) / (1 - i)) by XREAL_1:19;
then A41: (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0)) * |.fy.| < (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0)) * (|.fx.| + ((r0 / 2) / (1 - i))) by A13, XREAL_1:68;
(((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0)) * (|.fx.| + ((r0 / 2) / (1 - i))) = (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0)) * (|.fx.| + (r0 / (2 * (1 - i)))) by XCMPLX_1:78
.= (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0)) * (((|.fx.| * (2 * (1 - i))) / (2 * (1 - i))) + (r0 / (2 * (1 - i)))) by A27, XCMPLX_1:89
.= (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0)) * (((|.fx.| * (2 * (1 - i))) + r0) / (2 * (1 - i))) by XCMPLX_1:62
.= ((1 - i) * r0) / (2 * (1 - i)) by A7, A10, XCMPLX_1:98
.= r0 / 2 by A10, XCMPLX_1:91 ;
then A42: (abs (i - j)) * |.fy.| <= r0 / 2 by A34, A41, XXREAL_0:2;
fp = (1 - i) * x by A5
.= (1 - i) * fx by EUCLID:65 ;
then |.(fp - fe).| + |.(fe - fz).| < (r0 / 2) + (r0 / 2) by A36, A42, A40, XREAL_1:8;
then dist (ep,ez) < r0 by A37, XXREAL_0:2;
hence m in Ball (ep,r0) by A30, METRIC_1:11; :: thesis: verum

end;

hence F .: W c= V by A8, XBOOLE_1:1; :: thesis: verum

end;

suppose A43: 1 - i <= 0 ; :: thesis: ex W being Subset of [:(TOP-REAL n),I[01]:] st
( p in W & W is open & F .: W c= V )

A44: i <= 1 by BORSUK_1:43;
(1 - i) + i <= 0 + i by A43, XREAL_1:6;
then A45: i = 1 by A44, XXREAL_0:1;
set t = |.fx.| + r0;
reconsider B = Ball (lx,r0) as Subset of (TOP-REAL n) by TOPREAL3:8;
set c = r0 / (|.fx.| + r0);
set X1 = ].(1 - (r0 / (|.fx.| + r0))),1.];
A46: x in B by A7, GOBOARD6:1;
0 + r0 <= |.fx.| + r0 by XREAL_1:7;
then A47: r0 / (|.fx.| + r0) <= 1 by A7, XREAL_1:185;
then A48: (r0 / (|.fx.| + r0)) - (r0 / (|.fx.| + r0)) <= 1 - (r0 / (|.fx.| + r0)) by XREAL_1:9;
].(1 - (r0 / (|.fx.| + r0))),1.] c= the carrier of I[01]

proof

let s be set ; :: according to TARSKI:def 3 :: thesis: ( not s in ].(1 - (r0 / (|.fx.| + r0))),1.] or s in the carrier of I[01] )
assume A49: s in ].(1 - (r0 / (|.fx.| + r0))),1.] ; :: thesis: s in the carrier of I[01]
then reconsider s = s as Real ;
( s <= 1 & 1 - (r0 / (|.fx.| + r0)) < s ) by A49, XXREAL_1:2;
hence s in the carrier of I[01] by A48, BORSUK_1:43; :: thesis: verum

end;

then reconsider X1 = ].(1 - (r0 / (|.fx.| + r0))),1.] as Subset of I[01] ;
r0 / (|.fx.| + r0) is Point of I[01] by A7, A47, BORSUK_1:43;
then 1 - (r0 / (|.fx.| + r0)) is Point of I[01] by JORDAN5B:4;
then A50: X1 is open by Th4;
take W = [:B,X1:]; :: thesis: ( p in W & W is open & F .: W c= V )
A51: 0 < r0 / (|.fx.| + r0) by A7, XREAL_1:139;
then 1 - (r0 / (|.fx.| + r0)) < 1 - 0 by XREAL_1:15;
then i in X1 by A45, XXREAL_1:2;
hence p in W by A4, A46, ZFMISC_1:87; :: thesis: ( W is open & F .: W c= V )
r0 is Real by XREAL_0:def 1;
then B is open by A6, GOBOARD6:3;
hence W is open by A50, BORSUK_1:6; :: thesis: F .: W c= V
F .: W c= Ball (ep,r0)

proof

let m be set ; :: according to TARSKI:def 3 :: thesis: ( not m in F .: W or m in Ball (ep,r0) )
assume m in F .: W ; :: thesis: m in Ball (ep,r0)
then consider z being set such that
A52: z in dom F and
A53: z in W and
A54: F . z = m by FUNCT_1:def 6;
reconsider z = z as Point of [:(TOP-REAL n),I[01]:] by A52;
consider y being Point of (TOP-REAL n), j being Point of I[01] such that
A55: z = [y,j] by BORSUK_1:10;
reconsider ez = F . z, ey = y as Point of (Euclid n) by TOPREAL3:8;
reconsider fp = ep, fz = ez, fy = y as Element of REAL n by EUCLID:22;
fy in B by A53, A55, ZFMISC_1:87;
then A56: dist (lx,ey) < r0 by METRIC_1:11;
A57: ez = F . (y,j) by A55
.= (1 - j) * y by A1 ;
fp = (1 - i) * x by A5
.= 0. (TOP-REAL n) by A45, EUCLID:29 ;
then A58: fz - fp = (F . z) - (0. (TOP-REAL n)) by EUCLID:69
.= fz by RLVECT_1:13 ;
A59: |.fy.| - |.fx.| <= |.(fy - fx).| by EUCLID:15;
( dist (lx,ey) = |.(fx - fy).| & |.(fx - fy).| = |.(fy - fx).| ) by A6, EUCLID:18, SPPOL_1:5;
then |.fy.| - |.fx.| < r0 by A56, A59, XXREAL_0:2;
then A60: |.fy.| < |.fx.| + r0 by XREAL_1:19;

A61: now

per cases ( j < 1 or j >= 1 ) ;

suppose j < 1 ; :: thesis: (1 - j) * |.fy.| < r0

then A62: j - j < 1 - j by XREAL_1:14;
j in X1 by A53, A55, ZFMISC_1:87;
then 1 - (r0 / (|.fx.| + r0)) < j by XXREAL_1:2;
then (1 - (r0 / (|.fx.| + r0))) + (r0 / (|.fx.| + r0)) < j + (r0 / (|.fx.| + r0)) by XREAL_1:8;
then 1 - j < (j + (r0 / (|.fx.| + r0))) - j by XREAL_1:14;
then r0 / (1 - j) > r0 / (r0 / (|.fx.| + r0)) by A7, A62, XREAL_1:76;
then |.fx.| + r0 < r0 / (1 - j) by A51, XCMPLX_1:54;
then |.fy.| < r0 / (1 - j) by A60, XXREAL_0:2;
then (1 - j) * |.fy.| < (1 - j) * (r0 / (1 - j)) by A62, XREAL_1:68;
hence (1 - j) * |.fy.| < r0 by A62, XCMPLX_1:87; :: thesis: verum

end;

suppose A63: j >= 1 ; :: thesis: (1 - j) * |.fy.| < r0

j <= 1 by BORSUK_1:43;
then j = 1 by A63, XXREAL_0:1;
hence (1 - j) * |.fy.| < r0 by A7; :: thesis: verum

end;

end;

end;

1 - j is Point of I[01] by JORDAN5B:4;
then A64: 0 <= 1 - j by BORSUK_1:43;
dist (ep,ez) = |.(fz - fp).| by A6, SPPOL_1:5
.= |.fz.| by A58
.= |.((1 - j) * fy).| by A57, EUCLID:65
.= (abs (1 - j)) * |.fy.| by EUCLID:11
.= (1 - j) * |.fy.| by A64, ABSVALUE:def 1 ;
hence m in Ball (ep,r0) by A54, A61, METRIC_1:11; :: thesis: verum

end;

hence F .: W c= V by A8, XBOOLE_1:1; :: thesis: verum

end;

end;

end;

hence F is continuous by JGRAPH_2:10; :: thesis: verum