set X = east_halfline a;
reconsider XX = (east_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 (east_halfline a) ` holds
ex r being real number st
( r > 0 & Ball p,r c= (east_halfline a) ` )

proof

let p be Point of (Euclid 2); :: thesis: ( p in (east_halfline a) ` implies ex r being real number st
( r > 0 & Ball p,r c= (east_halfline a) ` ) )
reconsider x = p as Point of (TOP-REAL 2) by EUCLID:71;
assume p in (east_halfline a) ` ; :: thesis: ex r being real number st
( r > 0 & Ball p,r c= (east_halfline a) ` )
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 A33, TOPREAL1:def 13;

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

take r = abs ((x `2 ) - (a `2 )); :: thesis: ( r > 0 & Ball p,r c= (east_halfline a) ` )
(x `2 ) - (a `2 ) <> 0 by A34;
hence r > 0 by COMPLEX1:133; :: thesis: Ball p,r c= (east_halfline a) `
let b be set ; :: according to TARSKI:def 3 :: thesis: ( not b in Ball p,r or b in (east_halfline a) ` )
assume A35: b in Ball p,r ; :: thesis: b in (east_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 A35, METRIC_1:12;
then A36: dist x,c < r by TOPREAL6:def 1;

now

assume c `2 = a `2 ; :: thesis: contradiction
then A37: sqrt ((((x `1 ) - (c `1 )) ^2 ) + (((x `2 ) - (c `2 )) ^2 )) < abs ((x `2 ) - (c `2 )) by A36, TOPREAL6:101;
A38: 0 <= ((x `2 ) - (c `2 )) ^2 by XREAL_1:65;
A39: 0 <= ((x `1 ) - (c `1 )) ^2 by XREAL_1:65;
then 0 <= sqrt ((((x `1 ) - (c `1 )) ^2 ) + (((x `2 ) - (c `2 )) ^2 )) by A38, SQUARE_1:def 4;
then (sqrt ((((x `1 ) - (c `1 )) ^2 ) + (((x `2 ) - (c `2 )) ^2 ))) ^2 < (abs ((x `2 ) - (c `2 ))) ^2 by A37, 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 A38, SQUARE_1:def 4;
hence contradiction by A39, XREAL_1:9; :: thesis: verum

end;

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

end;

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

take r = (a `1 ) - (x `1 ); :: thesis: ( r > 0 & Ball p,r c= (east_halfline a) ` )
thus r > 0 by A40, XREAL_1:52; :: thesis: Ball p,r c= (east_halfline a) `
let b be set ; :: according to TARSKI:def 3 :: thesis: ( not b in Ball p,r or b in (east_halfline a) ` )
assume A41: b in Ball p,r ; :: thesis: b in (east_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 A41, METRIC_1:12;
then A42: dist x,c < r by TOPREAL6:def 1;

now

assume c `1 >= a `1 ; :: thesis: contradiction
then A43: (a `1 ) - (x `1 ) <= (c `1 ) - (x `1 ) by XREAL_1:15;
0 <= (a `1 ) - (x `1 ) by A40, XREAL_1:52;
then A44: ((a `1 ) - (x `1 )) ^2 <= ((c `1 ) - (x `1 )) ^2 by A43, SQUARE_1:77;
A45: 0 <= ((x `2 ) - (c `2 )) ^2 by XREAL_1:65;
A46: sqrt ((((x `1 ) - (c `1 )) ^2 ) + (((x `2 ) - (c `2 )) ^2 )) < (a `1 ) - (x `1 ) by A42, TOPREAL6:101;
A47: 0 <= ((x `1 ) - (c `1 )) ^2 by XREAL_1:65;
then 0 <= sqrt ((((x `1 ) - (c `1 )) ^2 ) + (((x `2 ) - (c `2 )) ^2 )) by A45, SQUARE_1:def 4;
then (sqrt ((((x `1 ) - (c `1 )) ^2 ) + (((x `2 ) - (c `2 )) ^2 ))) ^2 < ((a `1 ) - (x `1 )) ^2 by A46, SQUARE_1:78;
then A48: (((x `1 ) - (c `1 )) ^2 ) + (((x `2 ) - (c `2 )) ^2 ) < ((a `1 ) - (x `1 )) ^2 by A45, A47, SQUARE_1:def 4;
(((x `1 ) - (c `1 )) ^2 ) + 0 <= (((x `1 ) - (c `1 )) ^2 ) + (((x `2 ) - (c `2 )) ^2 ) by A45, XREAL_1:9;
hence contradiction by A48, A44, XXREAL_0:2; :: thesis: verum

end;

then not c in east_halfline a by TOPREAL1:def 13;
hence b in (east_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 east_halfline a is closed ; :: thesis: verum