theorem Th225: :: XXREAL_1:225

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