theorem Th227: :: XXREAL_1:227

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