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 A1: 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 K572(r,s) c= A )
assume that
A2: r in A and
A3: s in A ; :: thesis: K572(r,s) c= A
thus K572(r,s) c= A by A1, A2, A3; :: thesis: verum