theorem :: XXREAL_1:31

for p, q being ExtReal st p < q holds
not [.p,q.[ is empty by Th3;