theorem Th24: :: XXREAL_1:24

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