theorem :: XXREAL_1:269

for a, b being ExtReal holds ].-infty,b.[ /\ ].a,+infty.[ = ].a,b.[