let A be ext-real-membered set ; :: thesis: ( ( for y, r being ext-real number st y in A & inf A < r & r < y holds
r in A ) implies A is connected )
assume Z: for y, r being ext-real number st y in A & inf A < r & r < y holds
r in A ; :: thesis: A is connected
let x be ext-real number ; :: according to XXREAL_2:def 12 :: thesis: for s being ext-real number st x in A & s in A holds
[.x,s.] c= A
let y be ext-real number ; :: thesis: ( x in A & y in A implies [.x,y.] c= A )
assume Z1: ( x in A & y in A ) ; :: thesis: [.x,y.] c= A
let r be ext-real number ; :: according to MEMBERED:def 8 :: thesis: ( not r in [.x,y.] or r in A )
assume r in [.x,y.] ; :: thesis: r in A
then r in ].x,y.[ \/ {x,y} by XXREAL_1:29, XXREAL_1:128;
then pc: ( r in ].x,y.[ or r in {x,y} ) by XBOOLE_0:def 3;

per cases ( r = x or r = y or r in ].x,y.[ ) by pc, TARSKI:def 2;

suppose r = x ; :: thesis: r in A

hence r in A by Z1; :: thesis: verum

end;

suppose r = y ; :: thesis: r in A

hence r in A by Z1; :: thesis: verum

end;

suppose S: r in ].x,y.[ ; :: thesis: r in A

then A: x < r by XXREAL_1:4;
B: r < y by S, XXREAL_1:4;
inf A <= x by Z1, Th3;
then inf A < r by A, XXREAL_0:2;
hence r in A by B, Z, Z1; :: thesis: verum

end;

end;