let n be Element of NAT ; :: thesis: for s1 being Real
for P being Subset of (TOP-REAL n)
for i being Element of NAT st P = { p where p is Point of (TOP-REAL n) : s1 < p /. i } & i in Seg n holds
P is open
let s1 be Real; :: thesis: for P being Subset of (TOP-REAL n)
for i being Element of NAT st P = { p where p is Point of (TOP-REAL n) : s1 < p /. i } & i in Seg n holds
P is open
let P be Subset of (TOP-REAL n); :: thesis: for i being Element of NAT st P = { p where p is Point of (TOP-REAL n) : s1 < p /. i } & i in Seg n holds
P is open
let i be Element of NAT ; :: thesis: ( P = { p where p is Point of (TOP-REAL n) : s1 < p /. i } & i in Seg n implies P is open )
assume A1: ( P = { p where p is Point of (TOP-REAL n) : s1 < p /. i } & i in Seg n ) ; :: thesis: P is open
reconsider s1 = s1 as Real ;
A2: TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def 8;
then reconsider PP = P as Subset of (TopSpaceMetr (Euclid n)) ;
for pe being Point of (Euclid n) st pe in P holds
ex r being Real st
( r > 0 & Ball (pe,r) c= P )

proof

let pe be Point of (Euclid n); :: 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 p being Point of (TOP-REAL n) such that
A3: p = pe and
A4: s1 < p /. i by A1;
set r = ((p /. i) - s1) / 2;
A5: (p /. i) - s1 > 0 by A4, XREAL_1:50;
Ball (pe,(((p /. i) - s1) / 2)) c= P

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Ball (pe,(((p /. i) - s1) / 2)) or x in P )
assume x in Ball (pe,(((p /. i) - s1) / 2)) ; :: thesis: x in P
then x in { q where q is Element of (Euclid n) : dist (pe,q) < ((p /. i) - s1) / 2 } by METRIC_1:17;
then consider q being Element of (Euclid n) such that
A6: q = x and
A7: dist (pe,q) < ((p /. i) - s1) / 2 ;
reconsider ppe = pe, pq = q as Point of (TOP-REAL n) by TOPREAL3:8;
reconsider pen = ppe, pqn = pq as Element of REAL n ;
(Pitag_dist n) . (pe,q) = dist (pe,q) by METRIC_1:def 1;
then A8: |.(pen - pqn).| < ((p /. i) - s1) / 2 by A7, EUCLID:def 6;
reconsider qq = ppe - pq as Element of REAL n by EUCLID:22;
(ppe - pq) /. i <= |.qq.| by A1, Th11;
then (ppe - pq) /. i <= |.(pen - pqn).| ;
then (ppe - pq) /. i < ((p /. i) - s1) / 2 by A8, XXREAL_0:2;
then (ppe /. i) - (pq /. i) < ((p /. i) - s1) / 2 by A1, Th6;
then ((ppe /. i) - (pq /. i)) + (pq /. i) < (((p /. i) - s1) / 2) + (pq /. i) by XREAL_1:6;
then A9: (ppe /. i) - (((p /. i) - s1) / 2) < ((pq /. i) + (((p /. i) - s1) / 2)) - (((p /. i) - s1) / 2) by XREAL_1:9;
(p /. i) - (((p /. i) - s1) / 2) = s1 + (((p /. i) - s1) / 2) ;
then s1 < (p /. i) - (((p /. i) - s1) / 2) by A5, XREAL_1:29, XREAL_1:139;
then s1 < pq /. i by A3, A9, XXREAL_0:2;
hence x in P by A1, A6; :: thesis: verum

end;

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

end;

then PP is open by TOPMETR:15;
hence P is open by A2, PRE_TOPC:30; :: thesis: verum