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