theorem Th315: :: XXREAL_1:315

for p, q, r being ExtReal st r < p & p <= q holds
].r,q.] \ {p} = ].r,p.[ \/ ].p,q.]