theorem Th20: :: XXREAL_1:20

for r being ExtReal holds ].r,r.[ = {}