let q be ExtReal; :: thesis: for p being Real st p <= q holds
].-infty,q.] \ {p} = ].-infty,p.[ \/ ].p,q.]
let p be Real; :: thesis: ( p <= q implies ].-infty,q.] \ {p} = ].-infty,p.[ \/ ].p,q.] )
p in REAL by XREAL_0:def 1;
hence ( p <= q implies ].-infty,q.] \ {p} = ].-infty,p.[ \/ ].p,q.] ) by Th315, XXREAL_0:12; :: thesis: verum