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 Th337, Th224; :: thesis: verum