theorem Th21: :: XXREAL_1:21

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