theorem Th226: :: XXREAL_1:226

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