theorem :: XXREAL_1:389

for p being ExtReal holds REAL \ {p} = ].-infty,p.[ \/ ].p,+infty.[ by Th224, Th349, XXREAL_0:3;