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;
hence ( s <= q implies [.r,s.] c= ].-infty ,q.] ) by Th39, XXREAL_0:12; :: thesis: verum