let I be non empty Interval; :: thesis: for x being Real st inf I < x & x < sup I holds
ex Z being open Subset of REAL st
( x in Z & Z c= ].(inf I),(sup I).[ )
let x be Real; :: thesis: ( inf I < x & x < sup I implies ex Z being open Subset of REAL st
( x in Z & Z c= ].(inf I),(sup I).[ ) )
assume A1: ( inf I < x & x < sup I ) ; :: thesis: ex Z being open Subset of REAL st
( x in Z & Z c= ].(inf I),(sup I).[ )
then A2: inf I < sup I by XXREAL_0:2;

per cases ( inf I = -infty or inf I <> -infty ) ;

suppose A3: inf I = -infty ; :: thesis: ex Z being open Subset of REAL st
( x in Z & Z c= ].(inf I),(sup I).[ )

per cases ( sup I = +infty or sup I <> +infty ) ;

suppose A4: sup I = +infty ; :: thesis: ex Z being open Subset of REAL st
( x in Z & Z c= ].(inf I),(sup I).[ )

reconsider Z = ].(x - 1),(x + 1).[ as open Subset of REAL ;
take Z ; :: thesis: ( x in Z & Z c= ].(inf I),(sup I).[ )
( x - 1 < x & x < x + 1 ) by XREAL_1:29, XREAL_1:44;
hence x in Z by XXREAL_1:4; :: thesis: Z c= ].(inf I),(sup I).[

now :: thesis: for r being Real st r in Z holds
r in ].(inf I),(sup I).[

let r be Real; :: thesis: ( r in Z implies r in ].(inf I),(sup I).[ )
assume r in Z ; :: thesis: r in ].(inf I),(sup I).[
( inf I < r & r < sup I ) by A3, A4, XXREAL_0:4, XXREAL_0:6;
hence r in ].(inf I),(sup I).[ by XXREAL_1:4; :: thesis: verum

end;

hence Z c= ].(inf I),(sup I).[ ; :: thesis: verum

end;

suppose sup I <> +infty ; :: thesis: ex Z being open Subset of REAL st
( x in Z & Z c= ].(inf I),(sup I).[ )

then reconsider s = sup I as Real by A1, A3, XREAL_0:def 1, XXREAL_0:14;
A5: x - 1 < x by XREAL_1:44;
reconsider Z = ].(x - 1),s.[ as open Subset of REAL ;
take Z ; :: thesis: ( x in Z & Z c= ].(inf I),(sup I).[ )
thus x in Z by A5, A1, XXREAL_1:4; :: thesis: Z c= ].(inf I),(sup I).[

now :: thesis: for r being Real st r in Z holds
r in ].(inf I),(sup I).[

let r be Real; :: thesis: ( r in Z implies r in ].(inf I),(sup I).[ )
assume r in Z ; :: thesis: r in ].(inf I),(sup I).[
then ( inf I < r & r < sup I ) by A3, XXREAL_0:6, XXREAL_1:4;
hence r in ].(inf I),(sup I).[ by XXREAL_1:4; :: thesis: verum

end;

hence Z c= ].(inf I),(sup I).[ ; :: thesis: verum

end;

end;

end;

suppose A6: inf I <> -infty ; :: thesis: ex Z being open Subset of REAL st
( x in Z & Z c= ].(inf I),(sup I).[ )

then A7: -infty < inf I by XXREAL_0:6;
sup I <= +infty by XXREAL_0:3;
then reconsider i = inf I as Real by A2, A6, XXREAL_0:14, XREAL_0:def 1;

per cases ( sup I = +infty or sup I <> +infty ) ;

suppose A8: sup I = +infty ; :: thesis: ex Z being open Subset of REAL st
( x in Z & Z c= ].(inf I),(sup I).[ )

consider q being Real such that
A9: x < q by XREAL_1:1;
reconsider Z = ].i,q.[ as open Subset of REAL ;
take Z ; :: thesis: ( x in Z & Z c= ].(inf I),(sup I).[ )
thus x in Z by A1, A9, XXREAL_1:4; :: thesis: Z c= ].(inf I),(sup I).[

now :: thesis: for r being Real st r in Z holds
r in ].(inf I),(sup I).[

let r be Real; :: thesis: ( r in Z implies r in ].(inf I),(sup I).[ )
assume r in Z ; :: thesis: r in ].(inf I),(sup I).[
then ( inf I < r & r < sup I ) by A8, XXREAL_0:9, XXREAL_1:4;
hence r in ].(inf I),(sup I).[ by XXREAL_1:4; :: thesis: verum

end;

hence Z c= ].(inf I),(sup I).[ ; :: thesis: verum

end;

suppose sup I <> +infty ; :: thesis: ex Z being open Subset of REAL st
( x in Z & Z c= ].(inf I),(sup I).[ )

then reconsider s = sup I as Real by A7, A2, XREAL_0:def 1, XXREAL_0:14;
reconsider Z = ].i,s.[ as open Subset of REAL ;
take Z ; :: thesis: ( x in Z & Z c= ].(inf I),(sup I).[ )
thus x in Z by A1, XXREAL_1:4; :: thesis: Z c= ].(inf I),(sup I).[
thus Z c= ].(inf I),(sup I).[ ; :: thesis: verum

end;

end;

end;

end;