let A be ext-real-membered set ; ( A is interval implies for x, y, r being ExtReal st x in A & y in A & x <= r & r <= y holds
r in A )
assume A1:
A is interval
; for x, y, r being ExtReal st x in A & y in A & x <= r & r <= y holds
r in A
let x, y, r be ExtReal; ( x in A & y in A & x <= r & r <= y implies r in A )
assume that
A2:
x in A
and
A3:
y in A
and
A4:
x <= r
and
A5:
r <= y
; r in A
A6:
r in [.x,y.]
by A4, A5, XXREAL_1:1;
[.x,y.] c= A
by A1, A2, A3;
hence
r in A
by A6; verum