let A be ext-real-membered set ; :: thesis: ( A is empty implies A is connected )
assume Z: A is empty ; :: thesis: A is connected
let r be ext-real number ; :: according to XXREAL_2:def 12 :: thesis: for s being ext-real number st r in A & s in A holds
[.r,s.] c= A
let s be ext-real number ; :: thesis: ( r in A & s in A implies [.r,s.] c= A )
thus ( r in A & s in A implies [.r,s.] c= A ) by Z; :: thesis: verum