let a, b be ExtReal; :: thesis: ].a,b.[ is open
set A = ].a,b.[;

per cases ( ( a in REAL & b in REAL ) or a = +infty or ( a = -infty & b in REAL ) or ( a in REAL & b = +infty ) or b = -infty or ( a = -infty & b = +infty ) ) by XXREAL_0:14;

suppose ( a in REAL & b in REAL ) ; :: thesis: ].a,b.[ is open

then reconsider a = a, b = b as Real ;
].a,b.[ = ].-infty,b.[ /\ ].a,+infty.[ by XXREAL_1:269;
hence ].a,b.[ is open ; :: thesis: verum

end;

suppose a = +infty ; :: thesis: ].a,b.[ is open

then ].a,b.[ = {} by XXREAL_1:214;
hence ].a,b.[ is open ; :: thesis: verum

end;

suppose that A1: a = -infty and
A2: b in REAL ; :: thesis: ].a,b.[ is open

reconsider b = b as Real by A2;
].a,b.[ = left_open_halfline b by A1;
hence ].a,b.[ is open ; :: thesis: verum

end;

suppose that A3: a in REAL and
A4: b = +infty ; :: thesis: ].a,b.[ is open

reconsider a = a as Real by A3;
].a,b.[ = right_open_halfline a by A4;
hence ].a,b.[ is open ; :: thesis: verum

end;

suppose b = -infty ; :: thesis: ].a,b.[ is open

then ].a,b.[ = {} by XXREAL_1:210;
hence ].a,b.[ is open ; :: thesis: verum

end;

suppose ( a = -infty & b = +infty ) ; :: thesis: ].a,b.[ is open

then ].a,b.[ = [#] REAL by XXREAL_1:224;
hence ].a,b.[ is open ; :: thesis: verum

end;

end;