theorem :: BORSUK_5:61

for A being Subset of R^1
for a being Real st A = {a} holds
A ` = ].-infty,a.[ \/ ].a,+infty.[ by TOPMETR:17, XXREAL_1:389;