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