let A be ext-real-membered set ; :: thesis: ( ( for x, y, r being ExtReal st x in A & y in A & x <= r & r <= y holds

r in A ) implies A is interval )

assume for x, y, r being ExtReal st x in A & y in A & x <= r & r <= y holds

r in A ; :: thesis: A is interval

then for x, y, r being ExtReal st x in A & y in A & x < r & r < y holds

r in A ;

hence A is interval by Th84; :: thesis: verum

r in A ) implies A is interval )

assume for x, y, r being ExtReal st x in A & y in A & x <= r & r <= y holds

r in A ; :: thesis: A is interval

then for x, y, r being ExtReal st x in A & y in A & x < r & r < y holds

r in A ;

hence A is interval by Th84; :: thesis: verum