theorem :: XXREAL_1:271

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