let A be ext-real-membered set ; :: thesis: ( ( for y, r being ExtReal st y in A & inf A < r & r < y holds

r in A ) implies A is interval )

assume A1: for y, r being ExtReal st y in A & inf A < r & r < y holds

r in A ; :: thesis: A is interval

let x be ExtReal; :: according to XXREAL_2:def 12 :: thesis: for s being ExtReal st x in A & s in A holds

[.x,s.] c= A

let y be ExtReal; :: thesis: ( x in A & y in A implies [.x,y.] c= A )

assume that

A2: x in A and

A3: y in A ; :: thesis: [.x,y.] c= A

let r be ExtReal; :: 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 A4: ( r in ].x,y.[ or r in {x,y} ) by XBOOLE_0:def 3;

r in A ) implies A is interval )

assume A1: for y, r being ExtReal st y in A & inf A < r & r < y holds

r in A ; :: thesis: A is interval

let x be ExtReal; :: according to XXREAL_2:def 12 :: thesis: for s being ExtReal st x in A & s in A holds

[.x,s.] c= A

let y be ExtReal; :: thesis: ( x in A & y in A implies [.x,y.] c= A )

assume that

A2: x in A and

A3: y in A ; :: thesis: [.x,y.] c= A

let r be ExtReal; :: 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 A4: ( r in ].x,y.[ or r in {x,y} ) by XBOOLE_0:def 3;