take r ; :: according to XXREAL_2:def 9 :: thesis: r is LowerBound of [.r,s.[
let x be ExtReal; :: according to XXREAL_2:def 2 :: thesis: ( not x in [.r,s.[ or r <= x )
thus ( not x in [.r,s.[ or r <= x ) by XXREAL_1:3; :: thesis: verum