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 XXREAL_1:29, XXREAL_1:128;
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 A4, TARSKI:def 2;
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 A3, Th4;
then A7: r < sup A by A6, XXREAL_0:2;
A8: x < r by A5, XXREAL_1:4;
inf A <= x by A2, Th3;
then inf A < r by A8, XXREAL_0:2;
hence r in A by A1, A7; :: thesis: verum
end;
end;