let r be ext-real number ; :: according to XXREAL_2:def 12 :: thesis: for s being ext-real number st r in ExtREAL & s in ExtREAL holds
[.r,s.] c= ExtREAL
let s be ext-real number ; :: thesis: ( r in ExtREAL & s in ExtREAL implies [.r,s.] c= ExtREAL )
thus ( r in ExtREAL & s in ExtREAL implies [.r,s.] c= ExtREAL ) by MEMBERED:2; :: thesis: verum