let A be ext-real-membered set ; ( ( 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
; 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; verum