let A be ext-real-membered set ; :: thesis: ( ( for x, y, r being ext-real number st x in A & y in A & x <= r & r <= y holds
r in A ) implies A is connected )
assume for x, y, r being ext-real number st x in A & y in A & x <= r & r <= y holds
r in A ; :: thesis: A is connected
then for x, y, r being ext-real number st x in A & y in A & x < r & r < y holds
r in A ;
hence A is connected by Th88; :: thesis: verum