let s1 be Real; for P being Subset of (TOP-REAL 2) st P = { |[s,t]| where s, t is Real : s1 < s } holds
P is open
let P be Subset of (TOP-REAL 2); ( P = { |[s,t]| where s, t is Real : s1 < s } implies P is open )
assume A1:
P = { |[s,t]| where s, t is Real : s1 < s }
; 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 < s
by A1;
set r =
(s - s1) / 2;
A4:
s - s1 > 0
by A3, XREAL_1:52;
then A5:
(s - s1) / 2
> 0
by XREAL_1:141;
Ball pe,
((s - s1) / 2) c= P
proof
let x be
set ;
TARSKI:def 3 ( not x in Ball pe,((s - s1) / 2) or x in P )
assume
x in Ball pe,
((s - s1) / 2)
;
x in P
then
x in { q where q is Element of (Euclid 2) : dist pe,q < (s - s1) / 2 }
by METRIC_1:18;
then consider q being
Element of
(Euclid 2) such that A6:
q = x
and A7:
dist pe,
q < (s - s1) / 2
;
reconsider ppe =
pe,
pq =
q as
Point of
(TOP-REAL 2) by EUCLID:25;
(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 )) < (s - s1) / 2
by A7, TOPREAL3:12;
A9:
0 <= ((ppe `1 ) - (pq `1 )) ^2
by XREAL_1:65;
0 <= ((ppe `2 ) - (pq `2 )) ^2
by XREAL_1:65;
then A10:
0 + 0 <= (((ppe `1 ) - (pq `1 )) ^2 ) + (((ppe `2 ) - (pq `2 )) ^2 )
by A9, XREAL_1:9;
then
0 <= sqrt ((((ppe `1 ) - (pq `1 )) ^2 ) + (((ppe `2 ) - (pq `2 )) ^2 ))
by SQUARE_1:def 4;
then
(sqrt ((((ppe `1 ) - (pq `1 )) ^2 ) + (((ppe `2 ) - (pq `2 )) ^2 ))) ^2 < ((s - s1) / 2) ^2
by A8, SQUARE_1:78;
then A11:
(((ppe `1 ) - (pq `1 )) ^2 ) + (((ppe `2 ) - (pq `2 )) ^2 ) < ((s - s1) / 2) ^2
by A10, SQUARE_1:def 4;
((ppe `1 ) - (pq `1 )) ^2 <= (((ppe `1 ) - (pq `1 )) ^2 ) + (((ppe `2 ) - (pq `2 )) ^2 )
by XREAL_1:33, XREAL_1:65;
then
((ppe `1 ) - (pq `1 )) ^2 < ((s - s1) / 2) ^2
by A11, XXREAL_0:2;
then
(ppe `1 ) - (pq `1 ) < (s - s1) / 2
by A5, SQUARE_1:77;
then
ppe `1 < (pq `1 ) + ((s - s1) / 2)
by XREAL_1:21;
then
(ppe `1 ) - ((s - s1) / 2) < pq `1
by XREAL_1:21;
then A12:
s - ((s - s1) / 2) < pq `1
by A2, EUCLID:56;
s - ((s - s1) / 2) = ((s - s1) / 2) + s1
;
then A13:
s1 < s - ((s - s1) / 2)
by A4, XREAL_1:31, XREAL_1:141;
A14:
|[(pq `1 ),(pq `2 )]| = x
by A6, EUCLID:57;
s1 < pq `1
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:141;
verum
end;
then
PP is open
by TOPMETR:22;
hence
P is open
by Lm9, PRE_TOPC:60; verum