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 Th40; :: thesis: verum