let a, b be ExtReal; :: thesis: ].-infty,b.[ /\ ].a,+infty.[ = ].a,b.[
A1: -infty <= a by XXREAL_0:5;
b <= +infty by XXREAL_0:3;
hence ].-infty,b.[ /\ ].a,+infty.[ = ].a,b.[ by A1, Th160; :: thesis: verum