set X = east_halfline a;
reconsider XX = () ` as Subset of () ;
reconsider OO = XX as Subset of () by Lm3;
for p being Point of () st p in () ` holds
ex r being Real st
( r > 0 & Ball (p,r) c= () ` )
proof
let p be Point of (); :: thesis: ( p in () ` implies ex r being Real st
( r > 0 & Ball (p,r) c= () ` ) )

reconsider x = p as Point of () by EUCLID:67;
assume p in () ` ; :: thesis: ex r being Real st
( r > 0 & Ball (p,r) c= () ` )

then A33: not p in east_halfline a by XBOOLE_0:def 5;
per cases ( x `2 <> a `2 or x `1 < a `1 ) by ;
suppose A34: x `2 <> a `2 ; :: thesis: ex r being Real st
( r > 0 & Ball (p,r) c= () ` )

take r = |.((x `2) - (a `2)).|; :: thesis: ( r > 0 & Ball (p,r) c= () ` )
(x `2) - (a `2) <> 0 by A34;
hence r > 0 by COMPLEX1:47; :: thesis: Ball (p,r) c= () `
let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in Ball (p,r) or b in () ` )
assume A35: b in Ball (p,r) ; :: thesis: b in () `
then reconsider b = b as Point of () ;
reconsider c = b as Point of () by EUCLID:67;
dist (p,b) < r by ;
then A36: dist (x,c) < r by TOPREAL6:def 1;
now :: thesis: not c `2 = a `2
assume c `2 = a `2 ; :: thesis: contradiction
then A37: sqrt ((((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2)) < |.((x `2) - (c `2)).| by ;
A38: 0 <= ((x `2) - (c `2)) ^2 by XREAL_1:63;
A39: 0 <= ((x `1) - (c `1)) ^2 by XREAL_1:63;
then 0 <= sqrt ((((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2)) by ;
then (sqrt ((((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2))) ^2 < |.((x `2) - (c `2)).| ^2 by ;
then (sqrt ((((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2))) ^2 < ((x `2) - (c `2)) ^2 by COMPLEX1:75;
then (((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2) < (((x `2) - (c `2)) ^2) + 0 by ;
hence contradiction by A39, XREAL_1:7; :: thesis: verum
end;
then not c in east_halfline a by TOPREAL1:def 11;
hence b in () ` by XBOOLE_0:def 5; :: thesis: verum
end;
suppose A40: x `1 < a `1 ; :: thesis: ex r being Real st
( r > 0 & Ball (p,r) c= () ` )

take r = (a `1) - (x `1); :: thesis: ( r > 0 & Ball (p,r) c= () ` )
thus r > 0 by ; :: thesis: Ball (p,r) c= () `
let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in Ball (p,r) or b in () ` )
assume A41: b in Ball (p,r) ; :: thesis: b in () `
then reconsider b = b as Point of () ;
reconsider c = b as Point of () by EUCLID:67;
dist (p,b) < r by ;
then A42: dist (x,c) < r by TOPREAL6:def 1;
now :: thesis: not c `1 >= a `1
assume c `1 >= a `1 ; :: thesis: contradiction
then A43: (a `1) - (x `1) <= (c `1) - (x `1) by XREAL_1:13;
0 <= (a `1) - (x `1) by ;
then A44: ((a `1) - (x `1)) ^2 <= ((c `1) - (x `1)) ^2 by ;
A45: 0 <= ((x `2) - (c `2)) ^2 by XREAL_1:63;
A46: sqrt ((((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2)) < (a `1) - (x `1) by ;
A47: 0 <= ((x `1) - (c `1)) ^2 by XREAL_1:63;
then 0 <= sqrt ((((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2)) by ;
then (sqrt ((((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2))) ^2 < ((a `1) - (x `1)) ^2 by ;
then A48: (((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2) < ((a `1) - (x `1)) ^2 by ;
(((x `1) - (c `1)) ^2) + 0 <= (((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2) by ;
hence contradiction by A48, A44, XXREAL_0:2; :: thesis: verum
end;
then not c in east_halfline a by TOPREAL1:def 11;
hence b in () ` by XBOOLE_0:def 5; :: thesis: verum
end;
end;
end;
then OO is open by TOPMETR:15;
then XX is open by ;
then XX ` is closed ;
hence east_halfline a is closed ; :: thesis: verum