let A be ext-real-membered set ; :: thesis: ( A is connected implies for x, r being ext-real number st x in A & x <= r & r < sup A holds
r in A )
assume Z: A is connected ; :: thesis: for x, r being ext-real number st x in A & x <= r & r < sup A holds
r in A
let x, r be ext-real number ; :: thesis: ( x in A & x <= r & r < sup A implies r in A )
assume that
Z1: x in A and
Z3: x <= r and
Z4: r < sup A ; :: thesis: r in A

per cases ( ex y being ext-real number st
( y in A & r < y ) or for y being ext-real number holds
( not y in A or not r < y ) ) ;

suppose ex y being ext-real number st
( y in A & r < y ) ; :: thesis: r in A

hence r in A by Z, Z1, Z3, Th84; :: thesis: verum

end;

suppose for y being ext-real number holds
( not y in A or not r < y ) ; :: thesis: r in A

then r is UpperBound of A by Def1;
hence r in A by Z4, Def3; :: thesis: verum

end;

end;