let I be Interval; :: thesis: ( ].(inf I),(sup I).[ is open Subset of REAL & ].(inf I),(sup I).[ c= I )

now :: thesis: ].(inf I),(sup I).[ is open Subset of REAL

per cases ( ( inf I in REAL & sup I in REAL ) or not inf I in REAL or not sup I in REAL ) ;

suppose ( inf I in REAL & sup I in REAL ) ; :: thesis: ].(inf I),(sup I).[ is open Subset of REAL

then reconsider a = inf I, b = sup I as Real ;
].(inf I),(sup I).[ = ].a,b.[ ;
hence ].(inf I),(sup I).[ is open Subset of REAL ; :: thesis: verum

end;

suppose A1: not inf I in REAL ; :: thesis: ].(inf I),(sup I).[ is open Subset of REAL

per cases ( inf I = +infty or inf I = -infty ) by A1, XXREAL_0:14;

suppose A2: inf I = +infty ; :: thesis: ].(inf I),(sup I).[ is open Subset of REAL

].(inf I),(sup I).[ = {} by A2, XXREAL_0:3, XXREAL_1:28;
hence ].(inf I),(sup I).[ is open Subset of REAL ; :: thesis: verum

end;

suppose A3: inf I = -infty ; :: thesis: ].(inf I),(sup I).[ is open Subset of REAL

per cases ( sup I in REAL or not sup I in REAL ) ;

suppose sup I in REAL ; :: thesis: ].(inf I),(sup I).[ is open Subset of REAL

then reconsider b = sup I as Real ;
].(inf I),(sup I).[ = halfline b by A3, PROB_1:def 10;
hence ].(inf I),(sup I).[ is open Subset of REAL ; :: thesis: verum

end;

suppose A4: not sup I in REAL ; :: thesis: ].(inf I),(sup I).[ is open Subset of REAL

per cases ( sup I = +infty or sup I = -infty ) by A4, XXREAL_0:14;

suppose sup I = +infty ; :: thesis: ].(inf I),(sup I).[ is open Subset of REAL

then ].(inf I),(sup I).[ = [#] REAL by A3, XXREAL_1:224, SUBSET_1:def 3;
hence ].(inf I),(sup I).[ is open Subset of REAL ; :: thesis: verum

end;

suppose sup I = -infty ; :: thesis: ].(inf I),(sup I).[ is open Subset of REAL

then ].(inf I),(sup I).[ = {} by A3, XXREAL_1:20;
hence ].(inf I),(sup I).[ is open Subset of REAL ; :: thesis: verum

end;

end;

end;

end;

end;

end;

end;

suppose not sup I in REAL ; :: thesis: ].(inf I),(sup I).[ is open Subset of REAL

per cases then ( sup I = -infty or sup I = +infty ) by XXREAL_0:14;

suppose A6: sup I = -infty ; :: thesis: ].(inf I),(sup I).[ is open Subset of REAL

].(inf I),(sup I).[ = {} by A6, XXREAL_0:5, XXREAL_1:28;
hence ].(inf I),(sup I).[ is open Subset of REAL ; :: thesis: verum

end;

suppose A7: sup I = +infty ; :: thesis: ].(inf I),(sup I).[ is open Subset of REAL

per cases ( inf I in REAL or not inf I in REAL ) ;

suppose inf I in REAL ; :: thesis: ].(inf I),(sup I).[ is open Subset of REAL

then reconsider a = inf I as Real ;
].(inf I),(sup I).[ = right_open_halfline a by A7, LIMFUNC1:def 3;
hence ].(inf I),(sup I).[ is open Subset of REAL ; :: thesis: verum

end;

suppose A8: not inf I in REAL ; :: thesis: ].(inf I),(sup I).[ is open Subset of REAL

per cases ( inf I = -infty or inf I = +infty ) by A8, XXREAL_0:14;

suppose inf I = -infty ; :: thesis: ].(inf I),(sup I).[ is open Subset of REAL

then ].(inf I),(sup I).[ = [#] REAL by A7, XXREAL_1:224, SUBSET_1:def 3;
hence ].(inf I),(sup I).[ is open Subset of REAL ; :: thesis: verum

end;

suppose inf I = +infty ; :: thesis: ].(inf I),(sup I).[ is open Subset of REAL

then ].(inf I),(sup I).[ = {} by A7, XXREAL_1:20;
hence ].(inf I),(sup I).[ is open Subset of REAL ; :: thesis: verum

end;

end;

end;

end;

end;

end;

end;

end;

end;

hence ].(inf I),(sup I).[ is open Subset of REAL ; :: thesis: ].(inf I),(sup I).[ c= I

now :: thesis: for a being set st a in ].(inf I),(sup I).[ holds
a in I

let a be set ; :: thesis: ( a in ].(inf I),(sup I).[ implies a in I )
assume A9: a in ].(inf I),(sup I).[ ; :: thesis: a in I
then reconsider a1 = a as Real ;
( inf I < a1 & a1 < sup I ) by A9, XXREAL_1:4;
hence a in I by XXREAL_2:83; :: thesis: verum

end;

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