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) ` )
proof
let p be
Point of
(Euclid 2);
( 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) `
;
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;
suppose A40:
x `1 < a `1
;
ex r being Real st
( r > 0 & Ball (p,r) c= (east_halfline a) ` )take r =
(a `1) - (x `1);
( r > 0 & Ball (p,r) c= (east_halfline a) ` )thus
r > 0
by A40, XREAL_1:50;
Ball (p,r) c= (east_halfline a) ` let b be
object ;
TARSKI:def 3 ( not b in Ball (p,r) or b in (east_halfline a) ` )assume A41:
b in Ball (
p,
r)
;
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 not c `1 >= a `1 assume
c `1 >= a `1
;
contradictionthen 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;
verum end; then
not
c in east_halfline a
by TOPREAL1:def 11;
hence
b in (east_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
east_halfline a is closed
; verum