let A be ext-real-membered set ; :: thesis: ( ( for r being ExtReal st inf A < r & r < sup A holds
r in A ) implies A is interval )

assume A1: for r being ExtReal st inf A < r & r < sup A 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 ;
then A4: ( 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 ;
suppose r = x ; :: thesis: r in A
hence r in A by A2; :: thesis: verum
end;
suppose r = y ; :: thesis: r in A
hence r in A by A3; :: thesis: verum
end;
suppose A5: r in ].x,y.[ ; :: thesis: r in A
then A6: r < y by XXREAL_1:4;
y <= sup A by ;
then A7: r < sup A by ;
A8: x < r by ;
inf A <= x by ;
then inf A < r by ;
hence r in A by A1, A7; :: thesis: verum
end;
end;