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