theorem :: XXREAL_1:348

for s being ExtReal
for q being Real holds [.-infty,q.[ \ ].-infty,s.] = {-infty} \/ ].s,q.[