set X = west_halfline a;
reconsider XX = (west_halfline a) ` as Subset of (TOP-REAL 2) ;
reconsider OO = XX as Subset of (TopSpaceMetr (Euclid 2)) by Lm3;
for p being Point of (Euclid 2) st p in (west_halfline a) ` holds
ex r being real number st
( r > 0 & Ball (p,r) c= (west_halfline a) ` )

proof

let p be Point of (Euclid 2); :: thesis: ( p in (west_halfline a) ` implies ex r being real number st
( r > 0 & Ball (p,r) c= (west_halfline a) ` ) )
reconsider x = p as Point of (TOP-REAL 2) by EUCLID:71;
assume p in (west_halfline a) ` ; :: thesis: ex r being real number st
( r > 0 & Ball (p,r) c= (west_halfline a) ` )
then A49: not p in west_halfline a by XBOOLE_0:def 5;

per cases ( x `2 <> a `2 or x `1 > a `1 ) by A49, TOPREAL1:def 15;

suppose A50: x `2 <> a `2 ; :: thesis: ex r being real number st
( r > 0 & Ball (p,r) c= (west_halfline a) ` )

take r = abs ((x `2) - (a `2)); :: thesis: ( r > 0 & Ball (p,r) c= (west_halfline a) ` )
(x `2) - (a `2) <> 0 by A50;
hence r > 0 by COMPLEX1:133; :: thesis: Ball (p,r) c= (west_halfline a) `
let b be set ; :: according to TARSKI:def 3 :: thesis: ( not b in Ball (p,r) or b in (west_halfline a) ` )
assume A51: b in Ball (p,r) ; :: thesis: b in (west_halfline a) `
then reconsider b = b as Point of (Euclid 2) ;
reconsider c = b as Point of (TOP-REAL 2) by EUCLID:71;
dist (p,b) < r by A51, METRIC_1:12;
then A52: dist (x,c) < r by TOPREAL6:def 1;

now

assume c `2 = a `2 ; :: thesis: contradiction
then A53: sqrt ((((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2)) < abs ((x `2) - (c `2)) by A52, TOPREAL6:101;
A54: 0 <= ((x `2) - (c `2)) ^2 by XREAL_1:65;
A55: 0 <= ((x `1) - (c `1)) ^2 by XREAL_1:65;
then 0 <= sqrt ((((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2)) by A54, SQUARE_1:def 4;
then (sqrt ((((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2))) ^2 < (abs ((x `2) - (c `2))) ^2 by A53, SQUARE_1:78;
then (sqrt ((((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2))) ^2 < ((x `2) - (c `2)) ^2 by COMPLEX1:161;
then (((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2) < (((x `2) - (c `2)) ^2) + 0 by A54, SQUARE_1:def 4;
hence contradiction by A55, XREAL_1:9; :: thesis: verum

end;

then not c in west_halfline a by TOPREAL1:def 15;
hence b in (west_halfline a) ` by XBOOLE_0:def 5; :: thesis: verum

end;

suppose A56: x `1 > a `1 ; :: thesis: ex r being real number st
( r > 0 & Ball (p,r) c= (west_halfline a) ` )

take r = (x `1) - (a `1); :: thesis: ( r > 0 & Ball (p,r) c= (west_halfline a) ` )
thus r > 0 by A56, XREAL_1:52; :: thesis: Ball (p,r) c= (west_halfline a) `
let b be set ; :: according to TARSKI:def 3 :: thesis: ( not b in Ball (p,r) or b in (west_halfline a) ` )
assume A57: b in Ball (p,r) ; :: thesis: b in (west_halfline a) `
then reconsider b = b as Point of (Euclid 2) ;
reconsider c = b as Point of (TOP-REAL 2) by EUCLID:71;
dist (p,b) < r by A57, METRIC_1:12;
then A58: dist (x,c) < r by TOPREAL6:def 1;

now

assume c `1 <= a `1 ; :: thesis: contradiction
then A59: (x `1) - (c `1) >= (x `1) - (a `1) by XREAL_1:15;
0 <= (x `1) - (a `1) by A56, XREAL_1:52;
then A60: ((x `1) - (a `1)) ^2 <= ((x `1) - (c `1)) ^2 by A59, SQUARE_1:77;
A61: 0 <= ((x `2) - (c `2)) ^2 by XREAL_1:65;
A62: sqrt ((((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2)) < (x `1) - (a `1) by A58, TOPREAL6:101;
A63: 0 <= ((x `1) - (c `1)) ^2 by XREAL_1:65;
then 0 <= sqrt ((((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2)) by A61, SQUARE_1:def 4;
then (sqrt ((((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2))) ^2 < ((x `1) - (a `1)) ^2 by A62, SQUARE_1:78;
then A64: (((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2) < ((x `1) - (a `1)) ^2 by A61, A63, SQUARE_1:def 4;
0 + (((x `1) - (c `1)) ^2) <= (((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2) by A61, XREAL_1:9;
hence contradiction by A64, A60, XXREAL_0:2; :: thesis: verum

end;

then not c in west_halfline a by TOPREAL1:def 15;
hence b in (west_halfline a) ` by XBOOLE_0:def 5; :: thesis: verum

end;

end;

end;

then OO is open by TOPMETR:22;
then XX is open by Lm3, PRE_TOPC:60;
then XX ` is closed ;
hence west_halfline a is closed ; :: thesis: verum