for p, q being ExtReal st p < q holds
p in [.-infty,q.[ by XXREAL_0:5, Th3;