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 = (s1 - (p /. i)) / 2;
A5: s1 - (p /. i) > 0 by A4, XREAL_1:50;
Ball (pe,((s1 - (p /. i)) / 2)) c= P

proof

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