theorem Th23: :: XXREAL_1:23

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