theorem Th350: :: XXREAL_1:350

for q being ExtReal
for p being Real st p <= q holds
].-infty,q.] \ {p} = ].-infty,p.[ \/ ].p,q.]