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

r in A )

assume A1: A is interval ; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum