let H be Subset of RNS_Real; :: thesis: for I being open_interval Subset of REAL st H = I holds
H is open
let I be open_interval Subset of REAL; :: thesis: ( H = I implies H is open )
assume A1: H = I ; :: thesis: H is open
for x being Point of RNS_Real st x in H holds
ex N being Neighbourhood of x st N c= H

proof

let x be Point of RNS_Real; :: thesis: ( x in H implies ex N being Neighbourhood of x st N c= H )
assume A2: x in H ; :: thesis: ex N being Neighbourhood of x st N c= H
reconsider s = x as Real ;
reconsider s1 = s as R_eal by XXREAL_0:def 1;
consider a, b being R_eal such that
A3: I = ].a,b.[ by MEASURE5:def 2;
A4: ( a < s & s < b ) by A1, A2, A3, XXREAL_1:4;
then consider a1 being Real such that
A5: ( a < a1 & a1 < s1 ) by INTEGR26:18;
consider b1 being Real such that
A6: ( s1 < b1 & b1 < b ) by A4, INTEGR26:18;
set e = min ((b1 - s),(s - a1));
A7: ( a1 <= s - (min ((b1 - s),(s - a1))) & s + (min ((b1 - s),(s - a1))) <= b1 ) by XREAL_1:11, XREAL_1:19, XXREAL_0:17;
set N = { y where y is Point of RNS_Real : ||.(y - x).|| < min ((b1 - s),(s - a1)) } ;

now :: thesis: for z being object st z in { y where y is Point of RNS_Real : ||.(y - x).|| < min ((b1 - s),(s - a1)) } holds
z in the carrier of RNS_Real

let z be object ; :: thesis: ( z in { y where y is Point of RNS_Real : ||.(y - x).|| < min ((b1 - s),(s - a1)) } implies z in the carrier of RNS_Real )
assume z in { y where y is Point of RNS_Real : ||.(y - x).|| < min ((b1 - s),(s - a1)) } ; :: thesis: z in the carrier of RNS_Real
then ex y being Point of RNS_Real st
( z = y & ||.(y - x).|| < min ((b1 - s),(s - a1)) ) ;
hence z in the carrier of RNS_Real ; :: thesis: verum

end;

then reconsider N = { y where y is Point of RNS_Real : ||.(y - x).|| < min ((b1 - s),(s - a1)) } as Subset of RNS_Real by TARSKI:def 3;
( 0 < b1 - s & 0 < s - a1 ) by A5, A6, XREAL_1:50;
then A8: N is Neighbourhood of x by XXREAL_0:21, NFCONT_1:def 1;

now :: thesis: for z being object st z in N holds
z in H

let z be object ; :: thesis: ( z in N implies z in H )
assume z in N ; :: thesis: z in H
then consider y being Point of RNS_Real such that
A9: ( z = y & ||.(y - x).|| < min ((b1 - s),(s - a1)) ) ;
reconsider h = y as Real ;
h - s = y - x by DUALSP03:4;
then ||.(y - x).|| = |.(h - s).| by EUCLID:def 2;
then h in ].(s - (min ((b1 - s),(s - a1)))),(s + (min ((b1 - s),(s - a1)))).[ by A9, RCOMP_1:1;
then ( s - (min ((b1 - s),(s - a1))) < h & h < s + (min ((b1 - s),(s - a1))) ) by XXREAL_1:4;
then ( a1 <= h & h <= b1 ) by A7, XXREAL_0:2;
then ( a < h & h < b ) by A5, A6, XXREAL_0:2;
hence z in H by A9, A1, A3; :: thesis: verum

end;

then N c= H ;
hence ex N being Neighbourhood of x st N c= H by A8; :: thesis: verum

end;

hence H is open by NDIFF_1:4; :: thesis: verum