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 = (s1 - t) / 2;
s1 - t > 0 by A2, XREAL_1:52;
then A3: (s1 - t) / 2 > 0 by XREAL_1:141;
Ball pe,((s1 - t) / 2) c= P

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Ball pe,((s1 - t) / 2) or x in P )
assume x in Ball pe,((s1 - t) / 2) ; :: thesis: x in P
then x in { q where q is Element of (Euclid 2) : dist pe,q < (s1 - t) / 2 } by METRIC_1:18;
then consider q being Element of (Euclid 2) such that
A4: q = x and
A5: dist pe,q < (s1 - t) / 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 )) < (s1 - t) / 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 < ((s1 - t) / 2) ^2 by A6, SQUARE_1:78;
then A9: (((ppe `1 ) - (pq `1 )) ^2 ) + (((ppe `2 ) - (pq `2 )) ^2 ) < ((s1 - t) / 2) ^2 by A8, SQUARE_1:def 4;
((ppe `2 ) - (pq `2 )) ^2 <= (((ppe `1 ) - (pq `1 )) ^2 ) + (((ppe `2 ) - (pq `2 )) ^2 ) by A7, XREAL_1:33;
then ((pq `2 ) - (ppe `2 )) ^2 < ((s1 - t) / 2) ^2 by A9, XXREAL_0:2;
then (pq `2 ) - (ppe `2 ) < (s1 - t) / 2 by A3, SQUARE_1:77;
then (ppe `2 ) + ((s1 - t) / 2) > pq `2 by XREAL_1:21;
then A10: t + ((s1 - t) / 2) > pq `2 by A2, EUCLID:56;
t + ((s1 - t) / 2) = s1 - ((s1 - t) / 2) ;
then s1 > t + ((s1 - t) / 2) by A3, XREAL_1:46;
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