let A be ext-real-membered set ; :: thesis: ( A is connected implies for x, y, r being ext-real number st x in A & y in A & x <= r & r <= y holds
r in A )
assume Z:
A is connected
; :: thesis: for x, y, r being ext-real number st x in A & y in A & x <= r & r <= y holds
r in A
let x, y, r be ext-real number ; :: thesis: ( x in A & y in A & x <= r & r <= y implies r in A )
assume that
Z1:
x in A
and
Z2:
y in A
and
Z3:
x <= r
and
Z4:
r <= y
; :: thesis: r in A
A:
[.x,y.] c= A
by Z, Z1, Z2, Def12;
r in [.x,y.]
by Z3, Z4, XXREAL_1:1;
hence
r in A
by A; :: thesis: verum