theorem Th18: :: MEASUR12:18

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 & not ( p = s & A \/ B = [.r,q.[ ) holds
( q = r & A \/ B = [.p,s.[ )