theorem :: XXREAL_1:270

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