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

per cases by XXREAL_0:14;

suppose ( a in REAL & b in REAL ) ; :: thesis:

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

end;

suppose a = +infty ; :: thesis:

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

end;

suppose that A1: a = -infty and
A2: b in REAL ; :: thesis:

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

end;

suppose that A3: a in REAL and
A4: b = +infty ; :: thesis:

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

end;

suppose b = -infty ; :: thesis:

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

end;

suppose ( a = -infty & b = +infty ) ; :: thesis:

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

end;

end;