theorem Th25: :: XXREAL_1:25

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