let s1 be Real; :: thesis: { |[s,t]| where s, t is Real : s1 < t } is open Subset of (TOP-REAL 2)
reconsider P = { |[s,t]| where s, t is Real : s1 < t } as Subset of (REAL 2) by Lm6;
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); :: thesis: ( pe in P implies ex r being Real st
( r > 0 & Ball (pe,r) c= P ) )
assume pe in P ; :: thesis: 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 < t ;
set r = (t - s1) / 2;
A3: t - s1 > 0 by A2, XREAL_1:50;
then A4: (t - s1) / 2 > 0 by XREAL_1:139;
Ball (pe,((t - s1) / 2)) c= P

proof

let x be object ; :: 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:17;
then consider q being Element of (Euclid 2) such that
A5: q = x and
A6: dist (pe,q) < (t - s1) / 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)) < (t - s1) / 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 < ((t - s1) / 2) ^2 by A7, SQUARE_1:16;
then A10: (((ppe `1) - (pq `1)) ^2) + (((ppe `2) - (pq `2)) ^2) < ((t - s1) / 2) ^2 by A9, SQUARE_1:def 2;
((ppe `2) - (pq `2)) ^2 <= (((ppe `2) - (pq `2)) ^2) + (((ppe `1) - (pq `1)) ^2) by XREAL_1:31, XREAL_1:63;
then ((ppe `2) - (pq `2)) ^2 < ((t - s1) / 2) ^2 by A10, XXREAL_0:2;
then (ppe `2) - (pq `2) < (t - s1) / 2 by A4, SQUARE_1:15;
then ppe `2 < (pq `2) + ((t - s1) / 2) by XREAL_1:19;
then (ppe `2) - ((t - s1) / 2) < pq `2 by XREAL_1:19;
then A11: t - ((t - s1) / 2) < pq `2 by A1, EUCLID:52;
t - ((t - s1) / 2) = ((t - s1) / 2) + s1 ;
then A12: s1 < t - ((t - s1) / 2) by A3, XREAL_1:29, XREAL_1:139;
A13: |[(pq `1),(pq `2)]| = x by A5, EUCLID:53;
s1 < pq `2 by A11, A12, XXREAL_0:2;
hence x in P by A13; :: thesis: verum

end;

hence ex r being Real st
( r > 0 & Ball (pe,r) c= P ) by A3, XREAL_1:139; :: thesis: verum

end;

then PP is open by TOPMETR:15;
hence { |[s,t]| where s, t is Real : s1 < t } is open Subset of (TOP-REAL 2) by Lm9, PRE_TOPC:30; :: thesis: verum