let X be Subset of R^1; :: thesis: ( X is connected implies X is interval )
assume A2: X is connected ; :: thesis: X is interval
let a be ext-real number ; :: according to XXREAL_2:def 12 :: thesis: for b₁ being set holds
( not a in X or not b₁ in X or [.a,b₁.] c= X )
thus for b₁ being set holds
( not a in X or not b₁ in X or [.a,b₁.] c= X ) by A2, BORSUK_5:111; :: thesis: verum