let X be Subset of REAL ; :: thesis: ( X is open & X is bounded & ( for g1, g2 being real number st g1 in X & g2 in X holds
[.g1,g2.] c= X ) implies ex p, g being real number st X = ].p,g.[ )
assume that
A1: ( X is open & X is bounded ) and
A2: for g1, g2 being real number st g1 in X & g2 in X holds
[.g1,g2.] c= X ; :: thesis: ex p, g being real number st X = ].p,g.[

per cases ( X = {} or X <> {} ) ;

suppose A3: X = {} ; :: thesis: ex p, g being real number st X = ].p,g.[

take 1 ; :: thesis: ex g being real number st X = ].1,g.[
take 0 ; :: thesis: X = ].1,0 .[
thus X = ].1,0 .[ by A3, XXREAL_1:28; :: thesis: verum

end;

suppose A4: X <> {} ; :: thesis: ex p, g being real number st X = ].p,g.[

A5: ( X is bounded_below & X is bounded_above ) by A1;
take p = lower_bound X; :: thesis: ex g being real number st X = ].p,g.[
take g = upper_bound X; :: thesis: X = ].p,g.[

now

let r be Real; :: thesis: ( ( r in X implies r in ].p,g.[ ) & ( r in ].p,g.[ implies r in X ) )
thus ( r in X implies r in ].p,g.[ ) :: thesis: ( r in ].p,g.[ implies r in X )

proof

assume A6: r in X ; :: thesis: r in ].p,g.[
then A7: ( g <> r & p <> r ) by A1, Th43, Th44;
r <= g by A5, A6, SEQ_4:def 4;
then A8: r < g by A7, XXREAL_0:1;
p <= r by A5, A6, SEQ_4:def 5;
then p < r by A7, XXREAL_0:1;
hence r in ].p,g.[ by A8; :: thesis: verum

end;

assume r in ].p,g.[ ; :: thesis: r in X
then A9: ex s being Real st
( s = r & p < s & s < g ) ;
then g - r > 0 by XREAL_1:52;
then consider g2 being real number such that
A10: ( g2 in X & g - (g - r) < g2 ) by A4, A5, SEQ_4:def 4;
r - p > 0 by A9, XREAL_1:52;
then consider g1 being real number such that
A11: ( g1 in X & g1 < p + (r - p) ) by A4, A5, SEQ_4:def 5;
reconsider g1 = g1, g2 = g2 as Real by XREAL_0:def 1;
A12: r in { s where s is Real : ( g1 <= s & s <= g2 ) } by A10, A11;
[.g1,g2.] c= X by A2, A10, A11;
hence r in X by A12; :: thesis: verum

end;

hence X = ].p,g.[ by SUBSET_1:8; :: thesis: verum

end;

end;