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 st

( r > 0 & Ball (p,r) c= (east_halfline a) ` )

then XX is open by Lm3, PRE_TOPC:30;

then XX ` is closed ;

hence east_halfline a is closed ; :: thesis: verum

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 st

( r > 0 & Ball (p,r) c= (east_halfline a) ` )

proof

then
OO is open
by TOPMETR:15;
let p be Point of (Euclid 2); :: thesis: ( p in (east_halfline a) ` implies ex r being Real st

( r > 0 & Ball (p,r) c= (east_halfline a) ` ) )

reconsider x = p as Point of (TOP-REAL 2) by EUCLID:67;

assume p in (east_halfline a) ` ; :: thesis: ex r being Real st

( r > 0 & Ball (p,r) c= (east_halfline a) ` )

then A33: not p in east_halfline a by XBOOLE_0:def 5;

end;( r > 0 & Ball (p,r) c= (east_halfline a) ` ) )

reconsider x = p as Point of (TOP-REAL 2) by EUCLID:67;

assume p in (east_halfline a) ` ; :: thesis: ex r being Real 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 11;

end;

suppose A34:
x `2 <> a `2
; :: thesis: ex r being Real st

( r > 0 & Ball (p,r) c= (east_halfline a) ` )

( r > 0 & Ball (p,r) c= (east_halfline a) ` )

take r = |.((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:47; :: thesis: Ball (p,r) c= (east_halfline a) `

let b be object ; :: 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:67;

dist (p,b) < r by A35, METRIC_1:11;

then A36: dist (x,c) < r by TOPREAL6:def 1;

hence b in (east_halfline a) ` by XBOOLE_0:def 5; :: thesis: verum

end;(x `2) - (a `2) <> 0 by A34;

hence r > 0 by COMPLEX1:47; :: thesis: Ball (p,r) c= (east_halfline a) `

let b be object ; :: 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:67;

dist (p,b) < r by A35, METRIC_1:11;

then A36: dist (x,c) < r by TOPREAL6:def 1;

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

then
not c in east_halfline a
by TOPREAL1:def 11;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 A36, TOPREAL6:92;

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 A38, SQUARE_1:def 2;

then (sqrt ((((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2))) ^2 < |.((x `2) - (c `2)).| ^2 by A37, SQUARE_1:16;

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 A38, SQUARE_1:def 2;

hence contradiction by A39, XREAL_1:7; :: thesis: verum

end;then A37: sqrt ((((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2)) < |.((x `2) - (c `2)).| by A36, TOPREAL6:92;

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 A38, SQUARE_1:def 2;

then (sqrt ((((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2))) ^2 < |.((x `2) - (c `2)).| ^2 by A37, SQUARE_1:16;

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 A38, SQUARE_1:def 2;

hence contradiction by A39, XREAL_1:7; :: thesis: verum

hence b in (east_halfline a) ` by XBOOLE_0:def 5; :: thesis: verum

suppose A40:
x `1 < a `1
; :: thesis: ex r being Real st

( r > 0 & Ball (p,r) c= (east_halfline a) ` )

( 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:50; :: thesis: Ball (p,r) c= (east_halfline a) `

let b be object ; :: 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:67;

dist (p,b) < r by A41, METRIC_1:11;

then A42: dist (x,c) < r by TOPREAL6:def 1;

hence b in (east_halfline a) ` by XBOOLE_0:def 5; :: thesis: verum

end;thus r > 0 by A40, XREAL_1:50; :: thesis: Ball (p,r) c= (east_halfline a) `

let b be object ; :: 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:67;

dist (p,b) < r by A41, METRIC_1:11;

then A42: dist (x,c) < r by TOPREAL6:def 1;

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

then
not c in east_halfline a
by TOPREAL1:def 11;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 A40, XREAL_1:50;

then A44: ((a `1) - (x `1)) ^2 <= ((c `1) - (x `1)) ^2 by A43, SQUARE_1:15;

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 A42, TOPREAL6:92;

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 A45, SQUARE_1:def 2;

then (sqrt ((((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2))) ^2 < ((a `1) - (x `1)) ^2 by A46, SQUARE_1:16;

then A48: (((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2) < ((a `1) - (x `1)) ^2 by A45, A47, SQUARE_1:def 2;

(((x `1) - (c `1)) ^2) + 0 <= (((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2) by A45, XREAL_1:7;

hence contradiction by A48, A44, XXREAL_0:2; :: thesis: verum

end;then A43: (a `1) - (x `1) <= (c `1) - (x `1) by XREAL_1:13;

0 <= (a `1) - (x `1) by A40, XREAL_1:50;

then A44: ((a `1) - (x `1)) ^2 <= ((c `1) - (x `1)) ^2 by A43, SQUARE_1:15;

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 A42, TOPREAL6:92;

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 A45, SQUARE_1:def 2;

then (sqrt ((((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2))) ^2 < ((a `1) - (x `1)) ^2 by A46, SQUARE_1:16;

then A48: (((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2) < ((a `1) - (x `1)) ^2 by A45, A47, SQUARE_1:def 2;

(((x `1) - (c `1)) ^2) + 0 <= (((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2) by A45, XREAL_1:7;

hence contradiction by A48, A44, XXREAL_0:2; :: thesis: verum

hence b in (east_halfline a) ` by XBOOLE_0:def 5; :: thesis: verum

then XX is open by Lm3, PRE_TOPC:30;

then XX ` is closed ;

hence east_halfline a is closed ; :: thesis: verum