theorem Th20: :: MEASUR12:20
for A, B being non empty Interval
for p, q, r, s being R_eal st A = [.p,q.[ & B = ].r,s.[ & A misses B & A \/ B is Interval holds
( p = s & A \/ B = ].r,q.[ )