theorem :: BORSUK_5:70

for a, b being Real holds ].-infty,a.] \/ {b} <> REAL