theorem Th21: :: MEASUR12:21

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.] )