theorem :: XXREAL_1:398

for s, p being Real holds REAL \ ].p,s.[ = ].-infty,p.] \/ [.s,+infty.[