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);
( 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) `
;
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 A8:
x `2 < a `2
;
ex r being Real st
( r > 0 & Ball (p,r) c= (north_halfline a) ` )take r =
(a `2) - (x `2);
( r > 0 & Ball (p,r) c= (north_halfline a) ` )thus
r > 0
by A8, XREAL_1:50;
Ball (p,r) c= (north_halfline a) ` let b be
object ;
TARSKI:def 3 ( not b in Ball (p,r) or b in (north_halfline a) ` )assume A9:
b in Ball (
p,
r)
;
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 not c `2 >= a `2 assume
c `2 >= a `2
;
contradictionthen 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;
verum end; then
not
c in north_halfline a
by TOPREAL1:def 10;
hence
b in (north_halfline a) `
by XBOOLE_0:def 5;
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
; verum