let A be ext-real-membered set ; :: thesis: ( A is interval implies for x, r being ExtReal st x in A & inf A < r & r <= x holds
r in A )
assume A1: A is interval ; :: thesis: for x, r being ExtReal st x in A & inf A < r & r <= x holds
r in A
let x, r be ExtReal; :: thesis: ( x in A & inf A < r & r <= x implies r in A )
assume that
A2: x in A and
A3: inf A < r and
A4: r <= x ; :: 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 ) ) ;

suppose ex y being ExtReal st
( y in A & r > y ) ; :: thesis: r in A

hence r in A by A1, A2, A4, Th80; :: thesis: verum

end;

suppose for y being ExtReal holds
( not y in A or not r > y ) ; :: thesis: r in A

then r is LowerBound of A by Def2;
hence r in A by A3, Def4; :: thesis: verum

end;

end;