theorem :: XXREAL_1:390

for p being Real holds ].-infty,+infty.] \ {p} = ].-infty,p.[ \/ ].p,+infty.] by Th350, XXREAL_0:3;