let s, p be Real; :: 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