theorem Th22: :: XXREAL_1:22

for p, q being ExtReal holds ].p,q.[ c= [.p,q.[