theorem Th8: :: RCOMP_3:8

for a, b being Real st a <= b holds
[.a,b.] /\ ((left_closed_halfline a) \/ (right_closed_halfline b)) = {a,b}