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