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

r in A )

assume A1: A is interval ; :: thesis: for x, r being ExtReal st x in A & x <= r & r < sup A holds

r in A

let x, r be ExtReal; :: thesis: ( x in A & x <= r & r < sup A implies r in A )

assume that

A2: x in A and

A3: x <= r and

A4: r < sup A ; :: thesis: r in A

r in A )

assume A1: A is interval ; :: thesis: for x, r being ExtReal st x in A & x <= r & r < sup A holds

r in A

let x, r be ExtReal; :: thesis: ( x in A & x <= r & r < sup A implies r in A )

assume that

A2: x in A and

A3: x <= r and

A4: r < sup A ; :: thesis: r in A

per cases
( ex y being ExtReal st

( y in A & r < y ) or for y being ExtReal holds

( not y in A or not r < y ) ) ;

( y in A & r < y ) or for y being ExtReal holds

( not y in A or not r < y ) ) ;

end;