let s1 be Real; { |[s,t]| where s, t is Real : s1 > s } is open Subset of (TOP-REAL 2)
reconsider P = { |[s,t]| where s, t is Real : s1 > s } as Subset of (REAL 2) by Lm3;
reconsider PP = P as Subset of (TopSpaceMetr (Euclid 2)) ;
for pe being Point of (Euclid 2) st pe in P holds
ex r being Real st
( r > 0 & Ball (pe,r) c= P )
proof
let pe be
Point of
(Euclid 2);
( pe in P implies ex r being Real st
( r > 0 & Ball (pe,r) c= P ) )
assume
pe in P
;
ex r being Real st
( r > 0 & Ball (pe,r) c= P )
then consider s,
t being
Real such that A1:
|[s,t]| = pe
and A2:
s1 > s
;
set r =
(s1 - s) / 2;
A3:
s1 - s > 0
by A2, XREAL_1:50;
then A4:
(s1 - s) / 2
> 0
by XREAL_1:139;
Ball (
pe,
((s1 - s) / 2))
c= P
proof
let x be
object ;
TARSKI:def 3 ( not x in Ball (pe,((s1 - s) / 2)) or x in P )
assume
x in Ball (
pe,
((s1 - s) / 2))
;
x in P
then
x in { q where q is Element of (Euclid 2) : dist (pe,q) < (s1 - s) / 2 }
by METRIC_1:17;
then consider q being
Element of
(Euclid 2) such that A5:
q = x
and A6:
dist (
pe,
q)
< (s1 - s) / 2
;
reconsider ppe =
pe,
pq =
q as
Point of
(TOP-REAL 2) by EUCLID:22;
(Pitag_dist 2) . (
pe,
q)
= dist (
pe,
q)
by METRIC_1:def 1;
then A7:
sqrt ((((ppe `1) - (pq `1)) ^2) + (((ppe `2) - (pq `2)) ^2)) < (s1 - s) / 2
by A6, TOPREAL3:7;
A8:
0 <= ((ppe `1) - (pq `1)) ^2
by XREAL_1:63;
0 <= ((ppe `2) - (pq `2)) ^2
by XREAL_1:63;
then A9:
0 + 0 <= (((ppe `1) - (pq `1)) ^2) + (((ppe `2) - (pq `2)) ^2)
by A8, XREAL_1:7;
then
0 <= sqrt ((((ppe `1) - (pq `1)) ^2) + (((ppe `2) - (pq `2)) ^2))
by SQUARE_1:def 2;
then
(sqrt ((((ppe `1) - (pq `1)) ^2) + (((ppe `2) - (pq `2)) ^2))) ^2 < ((s1 - s) / 2) ^2
by A7, SQUARE_1:16;
then A10:
(((ppe `1) - (pq `1)) ^2) + (((ppe `2) - (pq `2)) ^2) < ((s1 - s) / 2) ^2
by A9, SQUARE_1:def 2;
((ppe `1) - (pq `1)) ^2 <= (((ppe `1) - (pq `1)) ^2) + (((ppe `2) - (pq `2)) ^2)
by XREAL_1:31, XREAL_1:63;
then
((pq `1) - (ppe `1)) ^2 < ((s1 - s) / 2) ^2
by A10, XXREAL_0:2;
then
(pq `1) - (ppe `1) < (s1 - s) / 2
by A4, SQUARE_1:15;
then
(ppe `1) + ((s1 - s) / 2) > pq `1
by XREAL_1:19;
then A11:
s + ((s1 - s) / 2) > pq `1
by A1, EUCLID:52;
s + ((s1 - s) / 2) = s1 - ((s1 - s) / 2)
;
then A12:
s1 > s + ((s1 - s) / 2)
by A3, XREAL_1:44, XREAL_1:139;
A13:
|[(pq `1),(pq `2)]| = x
by A5, EUCLID:53;
s1 > pq `1
by A11, A12, XXREAL_0:2;
hence
x in P
by A13;
verum
end;
hence
ex
r being
Real st
(
r > 0 &
Ball (
pe,
r)
c= P )
by A3, XREAL_1:139;
verum
end;
then
PP is open
by TOPMETR:15;
hence
{ |[s,t]| where s, t is Real : s1 > s } is open Subset of (TOP-REAL 2)
by Lm9, PRE_TOPC:30; verum