let s, q be ext-real number ; :: thesis: for r being real number st s <= q holds
[.r,s.[ c= ].-infty ,q.[
let r be real number ; :: thesis: ( s <= q implies [.r,s.[ c= ].-infty ,q.[ )
r in REAL by XREAL_0:def 1;
then -infty < r by XXREAL_0:12;
hence ( s <= q implies [.r,s.[ c= ].-infty ,q.[ ) by Th48; :: thesis: verum