theorem :: XXREAL_1:33

for p, q being ExtReal st p < q holds
not ].p,q.[ is empty