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

proof

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

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

suppose A2: x `1 <> a `1 ; :: thesis: ex r being Real st
( r > 0 & Ball (p,r) c= (north_halfline a) ` )

take r = |.((x `1) - (a `1)).|; :: thesis: ( r > 0 & Ball (p,r) c= (north_halfline a) ` )
(x `1) - (a `1) <> 0 by A2;
hence r > 0 by COMPLEX1:47; :: thesis: Ball (p,r) c= (north_halfline a) `
let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in Ball (p,r) or b in (north_halfline a) ` )
assume A3: b in Ball (p,r) ; :: thesis: b in (north_halfline a) `
then reconsider bb = b as Point of (Euclid 2) ;
reconsider c = bb as Point of (TOP-REAL 2) by EUCLID:67;
dist (p,bb) < r by A3, METRIC_1:11;
then A4: dist (x,c) < r by TOPREAL6:def 1;

now :: thesis: not c `1 = a `1

assume c `1 = a `1 ; :: thesis: contradiction
then A5: sqrt ((((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2)) < |.((x `1) - (c `1)).| by A4, TOPREAL6:92;
A6: 0 <= ((x `1) - (c `1)) ^2 by XREAL_1:63;
A7: 0 <= ((x `2) - (c `2)) ^2 by XREAL_1:63;
then 0 <= sqrt ((((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2)) by A6, SQUARE_1:def 2;
then (sqrt ((((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2))) ^2 < |.((x `1) - (c `1)).| ^2 by A5, SQUARE_1:16;
then (sqrt ((((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2))) ^2 < ((x `1) - (c `1)) ^2 by COMPLEX1:75;
then (((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2) < (((x `1) - (c `1)) ^2) + 0 by A6, SQUARE_1:def 2;
hence contradiction by A7, XREAL_1:7; :: thesis: verum

end;

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

end;

suppose A8: x `2 < a `2 ; :: thesis: ex r being Real st
( r > 0 & Ball (p,r) c= (north_halfline a) ` )

take r = (a `2) - (x `2); :: thesis: ( r > 0 & Ball (p,r) c= (north_halfline a) ` )
thus r > 0 by A8, XREAL_1:50; :: thesis: Ball (p,r) c= (north_halfline a) `
let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in Ball (p,r) or b in (north_halfline a) ` )
assume A9: b in Ball (p,r) ; :: thesis: b in (north_halfline a) `
then reconsider b = b as Point of (Euclid 2) ;
reconsider c = b as Point of (TOP-REAL 2) by EUCLID:67;
dist (p,b) < r by A9, METRIC_1:11;
then A10: dist (x,c) < r by TOPREAL6:def 1;

now :: thesis: not c `2 >= a `2

assume c `2 >= a `2 ; :: thesis: contradiction
then A11: (a `2) - (x `2) <= (c `2) - (x `2) by XREAL_1:13;
0 <= (a `2) - (x `2) by A8, XREAL_1:50;
then A12: ((a `2) - (x `2)) ^2 <= ((c `2) - (x `2)) ^2 by A11, SQUARE_1:15;
A13: 0 <= ((x `1) - (c `1)) ^2 by XREAL_1:63;
A14: sqrt ((((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2)) < (a `2) - (x `2) by A10, TOPREAL6:92;
A15: 0 <= ((x `2) - (c `2)) ^2 by XREAL_1:63;
then 0 <= sqrt ((((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2)) by A13, SQUARE_1:def 2;
then (sqrt ((((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2))) ^2 < ((a `2) - (x `2)) ^2 by A14, SQUARE_1:16;
then A16: (((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2) < ((a `2) - (x `2)) ^2 by A13, A15, SQUARE_1:def 2;
0 + (((x `2) - (c `2)) ^2) <= (((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2) by A13, XREAL_1:7;
hence contradiction by A16, A12, XXREAL_0:2; :: thesis: verum

end;

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

end;

end;

end;

then OO is open by TOPMETR:15;
then XX is open by Lm3, PRE_TOPC:30;
then XX ` is closed ;
hence north_halfline a is closed ; :: thesis: verum