let X be LinearTopSpace; :: thesis:
let K be compact Subset of X; :: thesis:
let C be closed Subset of X; :: thesis:
assume A1: K misses C ; :: thesis:

suppose A2: K = {} ; :: thesis:

take V = [#] X; :: thesis:
thus V is a_neighborhood of 0. X by TOPGRP_1:21; :: thesis:
K + V = {} by A2, CONVEX1:40;
hence K + V misses C + V ; :: thesis:

end;

suppose A3: K <> {} ; :: thesis:

set xV = { [x,Vx] where x is Point of X, Vx is open a_neighborhood of 0. X : ( x in K & Vx is symmetric & ((x + Vx) + Vx) + Vx misses C ) } ;

A4: now :: thesis:

let x be Point of X; :: thesis:
assume A5: x in K ; :: thesis:
( (- x) + (C `) = { ((- x) + u) where u is Point of X : u in C ` } & K c= C ` ) by A1, RUSUB_4:def 8, SUBSET_1:23;
then (- x) + x in (- x) + (C `) by A5;
then 0. X in (- x) + (C `) by RLVECT_1:5;
then (- x) + (C `) is a_neighborhood of 0. X by CONNSP_2:3;
then consider V9 being open a_neighborhood of 0. X such that
V9 is symmetric and
A6: V9 + V9 c= (- x) + (C `) by Th56;
consider Vx being open a_neighborhood of 0. X such that
A7: Vx is symmetric and
A8: Vx + Vx c= V9 by Th56;
take Vx = Vx; :: thesis:
thus Vx is symmetric by A7; :: thesis:
Vx c= V9

proof

let z be object ; :: according to TARSKI:def 3 :: thesis:
assume A9: z in Vx ; :: thesis:
then reconsider z = z as Point of X ;
0. X in Vx by CONNSP_2:4;
then z + (0. X) in Vx + Vx by A9, Th3;
then z in Vx + Vx ;
hence z in V9 by A8; :: thesis:

end;

then Vx + (Vx + Vx) c= V9 + V9 by A8, Th11;
then (Vx + Vx) + Vx c= (- x) + (C `) by A6;
then x + ((Vx + Vx) + Vx) c= x + ((- x) + (C `)) by Th8;
then (x + Vx) + (Vx + Vx) c= x + ((- x) + (C `)) by Th7;
then ((x + Vx) + Vx) + Vx c= x + ((- x) + (C `)) by CONVEX1:36;
then ((x + Vx) + Vx) + Vx c= (x + (- x)) + (C `) by Th6;
then ((x + Vx) + Vx) + Vx c= (0. X) + (C `) by RLVECT_1:def 10;
then ((x + Vx) + Vx) + Vx c= C ` by Th5;
hence ((x + Vx) + Vx) + Vx misses C by SUBSET_1:23; :: thesis:

end;

A10: now :: thesis:

consider x being object such that
A11: x in K by A3, XBOOLE_0:def 1;
reconsider x = x as Point of X by A11;
consider Vx being open a_neighborhood of 0. X such that
A12: ( Vx is symmetric & ((x + Vx) + Vx) + Vx misses C ) by A4, A11;
take z = [x,Vx]; :: thesis:
thus z in { [x,Vx] where x is Point of X, Vx is open a_neighborhood of 0. X : ( x in K & Vx is symmetric & ((x + Vx) + Vx) + Vx misses C ) } by A11, A12; :: thesis:

end;

defpred S₁[ object , object ] means ex v1, v2 being Point of X ex V1, V2 being open a_neighborhood of 0. X st
( $1 = [v1,V1] & $2 = [v2,V2] & v1 + V1 = v2 + V2 );
A13: for x, y, z being object st S₁[x,y] & S₁[y,z] holds
S₁[x,z]

proof

let x, y, z be object ; :: thesis:
given v1, v2 being Point of X, V1, V2 being open a_neighborhood of 0. X such that A14: x = [v1,V1] and
A15: y = [v2,V2] and
A16: v1 + V1 = v2 + V2 ; :: thesis:
given w1, w2 being Point of X, W1, W2 being open a_neighborhood of 0. X such that A17: y = [w1,W1] and
A18: ( z = [w2,W2] & w1 + W1 = w2 + W2 ) ; :: thesis:
take v1 ; :: thesis:
take w2 ; :: thesis:
take V1 ; :: thesis:
take W2 ; :: thesis:
v2 = w1 by A15, A17, XTUPLE_0:1;
hence ( x = [v1,V1] & z = [w2,W2] & v1 + V1 = w2 + W2 ) by A14, A15, A16, A17, A18, XTUPLE_0:1; :: thesis:

end;

reconsider xV = { [x,Vx] where x is Point of X, Vx is open a_neighborhood of 0. X : ( x in K & Vx is symmetric & ((x + Vx) + Vx) + Vx misses C ) } as non empty set by A10;
A19: for x being object st x in xV holds
S₁[x,x]

proof

let x be object ; :: thesis:
assume x in xV ; :: thesis:
then ex v being Point of X ex V being open a_neighborhood of 0. X st
( x = [v,V] & v in K & V is symmetric & ((v + V) + V) + V misses C ) ;
hence S₁[x,x] ; :: thesis:

end;

A20: for x, y being object st S₁[x,y] holds
S₁[y,x] ;
consider eqR being Equivalence_Relation of xV such that
A21: for x, y being object holds
( [x,y] in eqR iff ( x in xV & y in xV & S₁[x,y] ) ) from EQREL_1:sch 1(A19, A20, A13);

now :: thesis:

let X be set ; :: thesis:
assume X in Class eqR ; :: thesis:
then ex x being object st
( x in xV & X = Class (eqR,x) ) by EQREL_1:def 3;
hence X <> {} by EQREL_1:20; :: thesis:

end;

then consider g being Function such that
A22: dom g = Class eqR and
A23: for X being set st X in Class eqR holds
g . X in X by FUNCT_1:111;
set xVV = rng g;
set F = { (x + Vx) where x is Point of X, Vx is open a_neighborhood of 0. X : [x,Vx] in rng g } ;
{ (x + Vx) where x is Point of X, Vx is open a_neighborhood of 0. X : [x,Vx] in rng g } c= bool the carrier of X

proof

let A be object ; :: according to TARSKI:def 3 :: thesis:
assume A in { (x + Vx) where x is Point of X, Vx is open a_neighborhood of 0. X : [x,Vx] in rng g } ; :: thesis:
then ex x being Point of X ex Vx being open a_neighborhood of 0. X st
( A = x + Vx & [x,Vx] in rng g ) ;
hence A in bool the carrier of X ; :: thesis:

end;

then reconsider F = { (x + Vx) where x is Point of X, Vx is open a_neighborhood of 0. X : [x,Vx] in rng g } as Subset-Family of X ;
A24: F is Cover of K

proof

let x be object ; :: according to TARSKI:def 3,SETFAM_1:def 11 :: thesis:
assume A25: x in K ; :: thesis:
then reconsider x = x as Point of X ;
consider Vx being open a_neighborhood of 0. X such that
A26: ( Vx is symmetric & ((x + Vx) + Vx) + Vx misses C ) by A4, A25;
[x,Vx] in xV by A25, A26;
then A27: Class (eqR,[x,Vx]) in Class eqR by EQREL_1:def 3;
then A28: g . (Class (eqR,[x,Vx])) in rng g by A22, FUNCT_1:def 3;
x + (0. X) in x + Vx by Lm1, CONNSP_2:4;
then A29: x in x + Vx ;
g . (Class (eqR,[x,Vx])) in Class (eqR,[x,Vx]) by A23, A27;
then [(g . (Class (eqR,[x,Vx]))),[x,Vx]] in eqR by EQREL_1:19;
then consider v1, v2 being Point of X, V1, V2 being open a_neighborhood of 0. X such that
A30: g . (Class (eqR,[x,Vx])) = [v1,V1] and
A31: [x,Vx] = [v2,V2] and
A32: v1 + V1 = v2 + V2 by A21;
( x = v2 & Vx = V2 ) by A31, XTUPLE_0:1;
then x + Vx in F by A30, A32, A28;
hence x in union F by A29, TARSKI:def 4; :: thesis:

end;

F is open

proof

let P be Subset of X; :: according to TOPS_2:def 1 :: thesis:
assume P in F ; :: thesis:
then ex x being Point of X ex Vx being open a_neighborhood of 0. X st
( P = x + Vx & [x,Vx] in rng g ) ;
hence P is open ; :: thesis:

end;

then consider G being Subset-Family of X such that
A33: G c= F and
A34: G is Cover of K and
A35: G is finite by A24, COMPTS_1:def 4;
set FVx = { Vx where Vx is open a_neighborhood of 0. X : ex x being Point of X st
( x + Vx in G & [x,Vx] in rng g ) } ;
{ Vx where Vx is open a_neighborhood of 0. X : ex x being Point of X st
( x + Vx in G & [x,Vx] in rng g ) } c= bool the carrier of X

proof

let A be object ; :: according to TARSKI:def 3 :: thesis:
assume A in { Vx where Vx is open a_neighborhood of 0. X : ex x being Point of X st
( x + Vx in G & [x,Vx] in rng g ) } ; :: thesis:
then ex Vx being open a_neighborhood of 0. X st
( A = Vx & ex x being Point of X st
( x + Vx in G & [x,Vx] in rng g ) ) ;
hence A in bool the carrier of X ; :: thesis:

end;

then reconsider FVx = { Vx where Vx is open a_neighborhood of 0. X : ex x being Point of X st
( x + Vx in G & [x,Vx] in rng g ) } as Subset-Family of X ;
defpred S₂[ object , object ] means ex x being Point of X ex Vx being open a_neighborhood of 0. X st
( $1 = x + Vx & x + Vx in G & [x,Vx] in rng g & $2 = Vx );
A36: for x being object st x in G holds
ex y being object st
( y in FVx & S₂[x,y] )

proof

let x be object ; :: thesis:
assume A37: x in G ; :: thesis:
then x in F by A33;
then consider z being Point of X, Vz being open a_neighborhood of 0. X such that
A38: ( x = z + Vz & [z,Vz] in rng g ) ;
take Vz ; :: thesis:
thus ( Vz in FVx & S₂[x,Vz] ) by A37, A38; :: thesis:

end;

consider f being Function of G,FVx such that
A39: for x being object st x in G holds
S₂[x,f . x] from FUNCT_2:sch 1(A36);
set FxVxVx = { ((x + Vx) + Vx) where x is Point of X, Vx is open a_neighborhood of 0. X : ( x + Vx in G & [x,Vx] in rng g ) } ;
take V = meet FVx; :: thesis:
A40: rng g c= xV

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in rng g ; :: thesis:
then consider y being object such that
A41: y in dom g and
A42: x = g . y by FUNCT_1:def 3;
reconsider y = y as set by TARSKI:1;
x in y by A22, A23, A41, A42;
hence x in xV by A22, A41; :: thesis:

end;

A43: for A being Subset of X st A in G holds
ex x being Point of X ex Vx being open a_neighborhood of 0. X st
( A = x + Vx & [x,Vx] in rng g )

proof

let A be Subset of X; :: thesis:
assume A in G ; :: thesis:
then A in F by A33;
hence ex x being Point of X ex Vx being open a_neighborhood of 0. X st
( A = x + Vx & [x,Vx] in rng g ) ; :: thesis:

end;

A44: now :: thesis:

consider y being Point of X such that
A45: y in K by A3, SUBSET_1:4;
consider W being Subset of X such that
y in W and
A46: W in G by A34, A45, Th2;
consider x being Point of X, Vx being open a_neighborhood of 0. X such that
A47: ( W = x + Vx & [x,Vx] in rng g ) by A43, A46;
Vx in FVx by A46, A47;
hence ex z being set st z in FVx ; :: thesis:

end;

then A48: dom f = G by FUNCT_2:def 1;
A49: FVx c= rng f

proof

let z be object ; :: according to TARSKI:def 3 :: thesis:
assume z in FVx ; :: thesis:
then consider Vx being open a_neighborhood of 0. X such that
A50: z = Vx and
A51: ex x being Point of X st
( x + Vx in G & [x,Vx] in rng g ) ;
consider x being Point of X such that
A52: x + Vx in G and
A53: [x,Vx] in rng g by A51;
consider v being Point of X, Vv being open a_neighborhood of 0. X such that
A54: x + Vx = v + Vv and
v + Vv in G and
A55: [v,Vv] in rng g and
A56: f . (x + Vx) = Vv by A39, A52;
[[x,Vx],[v,Vv]] in eqR by A21, A40, A53, A54, A55;
then [x,Vx] in Class (eqR,[v,Vv]) by EQREL_1:19;
then A57: Class (eqR,[v,Vv]) = Class (eqR,[x,Vx]) by A40, A55, EQREL_1:23;
consider A being object such that
A58: A in dom g and
A59: [x,Vx] = g . A by A53, FUNCT_1:def 3;
consider a being object such that
A60: a in xV and
A61: A = Class (eqR,a) by A22, A58, EQREL_1:def 3;
[x,Vx] in Class (eqR,a) by A22, A23, A58, A59, A61;
then A62: Class (eqR,a) = Class (eqR,[x,Vx]) by A60, EQREL_1:23;
consider B being object such that
A63: B in dom g and
A64: [v,Vv] = g . B by A55, FUNCT_1:def 3;
consider b being object such that
A65: b in xV and
A66: B = Class (eqR,b) by A22, A63, EQREL_1:def 3;
[v,Vv] in Class (eqR,b) by A22, A23, A63, A64, A66;
then [x,Vx] = [v,Vv] by A57, A59, A64, A61, A65, A66, A62, EQREL_1:23;
then Vx = Vv by XTUPLE_0:1;
hence z in rng f by A48, A50, A52, A56, FUNCT_1:3; :: thesis:

end;

A67: for x being Point of X
for Vx being open a_neighborhood of 0. X st x + Vx in G & [x,Vx] in rng g holds
( x in K & Vx is symmetric & ((x + Vx) + Vx) + Vx misses C )

proof

let x be Point of X; :: thesis:
let Vx be open a_neighborhood of 0. X; :: thesis:
assume that
A68: x + Vx in G and
A69: [x,Vx] in rng g ; :: thesis:
consider A being object such that
A70: A in dom g and
A71: [x,Vx] = g . A by A69, FUNCT_1:def 3;
consider a being object such that
A72: a in xV and
A73: A = Class (eqR,a) by A22, A70, EQREL_1:def 3;
[x,Vx] in Class (eqR,a) by A22, A23, A70, A71, A73;
then A74: Class (eqR,a) = Class (eqR,[x,Vx]) by A72, EQREL_1:23;
x + Vx in F by A33, A68;
then consider v being Point of X, Vv being open a_neighborhood of 0. X such that
A75: x + Vx = v + Vv and
A76: [v,Vv] in rng g ;
[[x,Vx],[v,Vv]] in eqR by A21, A40, A69, A75, A76;
then [x,Vx] in Class (eqR,[v,Vv]) by EQREL_1:19;
then A77: Class (eqR,[v,Vv]) = Class (eqR,[x,Vx]) by A40, A76, EQREL_1:23;
consider B being object such that
A78: B in dom g and
A79: [v,Vv] = g . B by A76, FUNCT_1:def 3;
consider b being object such that
A80: b in xV and
A81: B = Class (eqR,b) by A22, A78, EQREL_1:def 3;
[v,Vv] in Class (eqR,b) by A22, A23, A78, A79, A81;
then A82: [x,Vx] = [v,Vv] by A77, A71, A79, A73, A80, A81, A74, EQREL_1:23;
then A83: Vx = Vv by XTUPLE_0:1;
[v,Vv] in xV by A40, A76;
then consider u being Point of X, Vu being open a_neighborhood of 0. X such that
A84: [u,Vu] = [v,Vv] and
A85: ( u in K & Vu is symmetric & ((u + Vu) + Vu) + Vu misses C ) ;
Vv = Vu by A84, XTUPLE_0:1;
hence ( x in K & Vx is symmetric & ((x + Vx) + Vx) + Vx misses C ) by A84, A85, A82, A83, XTUPLE_0:1; :: thesis:

end;

now :: thesis:

let Z be set ; :: thesis:

hereby :: thesis:

reconsider A = C + V as set ;
assume Z in {{}} ; :: thesis:
then A86: Z = {} by TARSKI:def 1;
consider y being Point of X such that
A87: y in K by A3, SUBSET_1:4;
consider W being Subset of X such that
y in W and
A88: W in G by A34, A87, Th2;
consider x being Point of X, Vx being open a_neighborhood of 0. X such that
A89: ( W = x + Vx & [x,Vx] in rng g ) by A43, A88;
A90: ((x + Vx) + Vx) + Vx misses C by A67, A88, A89;
reconsider B = (x + Vx) + Vx as set ;
take A = A; :: thesis:
take B = B; :: thesis:
thus A in {(C + V)} by TARSKI:def 1; :: thesis:
thus B in { ((x + Vx) + Vx) where x is Point of X, Vx is open a_neighborhood of 0. X : ( x + Vx in G & [x,Vx] in rng g ) } by A88, A89; :: thesis:
A91: Vx is symmetric by A67, A88, A89;

now :: thesis:

A92: C + V = { (u + v) where u, v is Point of X : ( u in C & v in V ) } by RUSUB_4:def 9;
assume A meets B ; :: thesis:
then consider z being object such that
A93: z in A and
A94: z in B by XBOOLE_0:3;
reconsider z = z as Point of X by A93;
consider u, v being Point of X such that
A95: z = u + v and
A96: u in C and
A97: v in V by A93, A92;
Vx in FVx by A88, A89;
then v in Vx by A97, SETFAM_1:def 1;
then - v in Vx by A91, Th25;
then A98: z + (- v) in ((x + Vx) + Vx) + Vx by A94, Th3;
z + (- v) = u + (v + (- v)) by A95, RLVECT_1:def 3
.= u + (0. X) by RLVECT_1:5
.= u ;
hence contradiction by A90, A96, A98, XBOOLE_0:3; :: thesis:

end;

hence Z = A /\ B by A86; :: thesis:

end;

given A, B being set such that A99: A in {(C + V)} and
A100: B in { ((x + Vx) + Vx) where x is Point of X, Vx is open a_neighborhood of 0. X : ( x + Vx in G & [x,Vx] in rng g ) } and
A101: Z = A /\ B ; :: thesis:
A102: A = C + V by A99, TARSKI:def 1;
consider x being Point of X, Vx being open a_neighborhood of 0. X such that
A103: B = (x + Vx) + Vx and
A104: ( x + Vx in G & [x,Vx] in rng g ) by A100;
A105: ((x + Vx) + Vx) + Vx misses C by A67, A104;
A106: Vx is symmetric by A67, A104;

now :: thesis:

A107: C + V = { (u + v) where u, v is Point of X : ( u in C & v in V ) } by RUSUB_4:def 9;
assume A meets B ; :: thesis:
then consider z being object such that
A108: z in A and
A109: z in B by XBOOLE_0:3;
reconsider z = z as Point of X by A99, A108;
consider u, v being Point of X such that
A110: z = u + v and
A111: u in C and
A112: v in V by A102, A108, A107;
Vx in FVx by A104;
then v in Vx by A112, SETFAM_1:def 1;
then - v in Vx by A106, Th25;
then A113: z + (- v) in ((x + Vx) + Vx) + Vx by A103, A109, Th3;
z + (- v) = u + (v + (- v)) by A110, RLVECT_1:def 3
.= u + (0. X) by RLVECT_1:5
.= u ;
hence contradiction by A105, A111, A113, XBOOLE_0:3; :: thesis:

end;

then A /\ B = {} ;
hence Z in {{}} by A101, TARSKI:def 1; :: thesis:

end;

then INTERSECTION ({(C + V)}, { ((x + Vx) + Vx) where x is Point of X, Vx is open a_neighborhood of 0. X : ( x + Vx in G & [x,Vx] in rng g ) } ) = {{}} by SETFAM_1:def 5;
then union (INTERSECTION ({(C + V)}, { ((x + Vx) + Vx) where x is Point of X, Vx is open a_neighborhood of 0. X : ( x + Vx in G & [x,Vx] in rng g ) } )) = {} by ZFMISC_1:25;
then (C + V) /\ (union { ((x + Vx) + Vx) where x is Point of X, Vx is open a_neighborhood of 0. X : ( x + Vx in G & [x,Vx] in rng g ) } ) = {} by SETFAM_1:25;
then A114: C + V misses union { ((x + Vx) + Vx) where x is Point of X, Vx is open a_neighborhood of 0. X : ( x + Vx in G & [x,Vx] in rng g ) } ;
A115: FVx is open

proof

let P be Subset of X; :: according to TOPS_2:def 1 :: thesis:
assume P in FVx ; :: thesis:
then ex Vx being open a_neighborhood of 0. X st
( P = Vx & ex x being Point of X st
( x + Vx in G & [x,Vx] in rng g ) ) ;
hence P is open ; :: thesis:

end;

f " FVx is finite by A35, FINSET_1:1;
then FVx is finite by A49, FINSET_1:9;
then V is open by A115, TOPS_2:20;
then A116: Int V = V by TOPS_1:23;

now :: thesis:

let A be set ; :: thesis:
assume A117: A in FVx ; :: thesis:
then reconsider A9 = A as Subset of X ;
ex Vx being open a_neighborhood of 0. X st
( A = Vx & ex x being Point of X st
( x + Vx in G & [x,Vx] in rng g ) ) by A117;
then ( Int A9 c= A9 & 0. X in Int A9 ) by CONNSP_2:def 1, TOPS_1:16;
hence 0. X in A ; :: thesis:

end;

then 0. X in V by A44, SETFAM_1:def 1;
hence V is a_neighborhood of 0. X by A116, CONNSP_2:def 1; :: thesis:
set FxVxV = { ((x + Vx) + V) where x is Point of X, Vx is open a_neighborhood of 0. X : ( x + Vx in G & [x,Vx] in rng g ) } ;
A118: union { ((x + Vx) + V) where x is Point of X, Vx is open a_neighborhood of 0. X : ( x + Vx in G & [x,Vx] in rng g ) } c= union { ((x + Vx) + Vx) where x is Point of X, Vx is open a_neighborhood of 0. X : ( x + Vx in G & [x,Vx] in rng g ) }

proof

let z be object ; :: according to TARSKI:def 3 :: thesis:
assume z in union { ((x + Vx) + V) where x is Point of X, Vx is open a_neighborhood of 0. X : ( x + Vx in G & [x,Vx] in rng g ) } ; :: thesis:
then consider Y being set such that
A119: z in Y and
A120: Y in { ((x + Vx) + V) where x is Point of X, Vx is open a_neighborhood of 0. X : ( x + Vx in G & [x,Vx] in rng g ) } by TARSKI:def 4;
consider x being Point of X, Vx being open a_neighborhood of 0. X such that
A121: Y = (x + Vx) + V and
A122: ( x + Vx in G & [x,Vx] in rng g ) by A120;
A123: (x + Vx) + Vx in { ((x + Vx) + Vx) where x is Point of X, Vx is open a_neighborhood of 0. X : ( x + Vx in G & [x,Vx] in rng g ) } by A122;
(x + Vx) + V = { (u + v) where u, v is Point of X : ( u in x + Vx & v in V ) } by RUSUB_4:def 9;
then consider u, v being Point of X such that
A124: z = u + v and
A125: u in x + Vx and
A126: v in V by A119, A121;
Vx in FVx by A122;
then v in Vx by A126, SETFAM_1:def 1;
then u + v in (x + Vx) + Vx by A125, Th3;
hence z in union { ((x + Vx) + Vx) where x is Point of X, Vx is open a_neighborhood of 0. X : ( x + Vx in G & [x,Vx] in rng g ) } by A124, A123, TARSKI:def 4; :: thesis:

end;

K + V c= union { ((x + Vx) + V) where x is Point of X, Vx is open a_neighborhood of 0. X : ( x + Vx in G & [x,Vx] in rng g ) }

proof

let z be object ; :: according to TARSKI:def 3 :: thesis:
A127: K + V = { (u + v) where u, v is Point of X : ( u in K & v in V ) } by RUSUB_4:def 9;
assume z in K + V ; :: thesis:
then consider u, v being Point of X such that
A128: z = u + v and
A129: u in K and
A130: v in V by A127;
consider Vu being Subset of X such that
A131: u in Vu and
A132: Vu in G by A34, A129, Th2;
consider x being Point of X, Vx being open a_neighborhood of 0. X such that
A133: Vu = x + Vx and
A134: [x,Vx] in rng g by A43, A132;
A135: (x + Vx) + V in { ((x + Vx) + V) where x is Point of X, Vx is open a_neighborhood of 0. X : ( x + Vx in G & [x,Vx] in rng g ) } by A132, A133, A134;
z in (x + Vx) + V by A128, A130, A131, A133, Th3;
hence z in union { ((x + Vx) + V) where x is Point of X, Vx is open a_neighborhood of 0. X : ( x + Vx in G & [x,Vx] in rng g ) } by A135, TARSKI:def 4; :: thesis:

end;

hence K + V misses C + V by A118, A114, XBOOLE_1:1, XBOOLE_1:63; :: thesis:

end;