theorem :: XXREAL_1:30

for r, s being ExtReal st r <= s holds
not [.r,s.] is empty by Th1;