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