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