theorem :: ISOMICHI:33

for a, b being Real st a < b holds
REAL = (].-infty,a.[ \/ [.a,b.]) \/ ].b,+infty.[