let n be Element of NAT ; :: thesis: for s1 being real number
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 > Proj p,i } & i in Seg n holds
P is open
let s1 be real number ; :: 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 > Proj 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 > Proj 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 > Proj p,i } & i in Seg n implies P is open )
assume A1: ( P = { p where p is Point of (TOP-REAL n) : s1 > Proj p,i } & i in Seg n ) ; :: thesis: P is open
XX: 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)) ;
reconsider s1 = s1 as Real by XREAL_0:def 1;
for pe being Point of (Euclid n) 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 n); :: 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 p being Point of (TOP-REAL n) such that
A2: ( p = pe & s1 > Proj p,i ) by A1;
set r = (s1 - (Proj p,i)) / 2;
s1 - (Proj p,i) > 0 by A2, XREAL_1:52;
then A3: (s1 - (Proj p,i)) / 2 > 0 by XREAL_1:141;
Ball pe,((s1 - (Proj p,i)) / 2) c= P

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Ball pe,((s1 - (Proj p,i)) / 2) or x in P )
assume x in Ball pe,((s1 - (Proj p,i)) / 2) ; :: thesis: x in P
then x in { q where q is Element of (Euclid n) : dist pe,q < (s1 - (Proj p,i)) / 2 } by METRIC_1:18;
then consider q being Element of (Euclid n) such that
A4: q = x and
A5: dist pe,q < (s1 - (Proj p,i)) / 2 ;
reconsider ppe = pe, pq = q as Point of (TOP-REAL n) by TOPREAL3:13;
reconsider pen = ppe, pqn = pq as Element of REAL n ;
(Pitag_dist n) . q,pe = dist q,pe by METRIC_1:def 1;
then A6: |.(pqn - pen).| < (s1 - (Proj p,i)) / 2 by A5, EUCLID:def 6;
reconsider q = pq - ppe as Element of REAL n by EUCLID:25;
Proj (pq - ppe),i <= |.q.| by A1, Th15;
then Proj (pq - ppe),i <= |.(pqn - pen).| by A1, EUCLID:73;
then Proj (pq - ppe),i < (s1 - (Proj p,i)) / 2 by A6, XXREAL_0:2;
then (Proj pq,i) - (Proj ppe,i) < (s1 - (Proj p,i)) / 2 by A1, Th7;
then A7: (Proj p,i) + ((s1 - (Proj p,i)) / 2) > Proj pq,i by A2, XREAL_1:21;
(Proj p,i) + ((s1 - (Proj p,i)) / 2) = s1 - ((s1 - (Proj p,i)) / 2) ;
then s1 > (Proj p,i) + ((s1 - (Proj p,i)) / 2) by A3, XREAL_1:46;
then ( pq = x & s1 > Proj pq,i ) by A4, A7, 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 PRE_TOPC:60, XX; :: thesis: verum