theorem :: XXREAL_1:32

for p, q being ExtReal st p < q holds
not ].p,q.] is empty by Th2;