let s, p be real number ; :: thesis: REAL \ ].p,s.[ = ].-infty ,p.] \/ [.s,+infty .[
p in REAL by XREAL_0:def 1;
then p < +infty by XXREAL_0:9;
hence REAL \ ].p,s.[ = ].-infty ,p.] \/ [.s,+infty .[ by Th333, Th224; :: thesis: verum