let X be Subset of REAL; :: thesis: ( X is open & X is real-bounded & ( for g1, g2 being Real st g1 in X & g2 in X holds
[.g1,g2.] c= X ) implies ex p, g being Real st X = ].p,g.[ )
assume that
A1: X is open and
A2: X is real-bounded and
A3: for g1, g2 being Real st g1 in X & g2 in X holds
[.g1,g2.] c= X ; :: thesis: ex p, g being Real st X = ].p,g.[
per cases ( X = {} or X <> {} ) ;
suppose A4: X = {} ; :: thesis: ex p, g being Real st X = ].p,g.[
take 1 ; :: thesis: ex g being Real st X = ].1,g.[
take 0 ; :: thesis: X = ].1,0.[
thus X = ].1,0.[ by A4, XXREAL_1:28; :: thesis: verum
end;
suppose A5: X <> {} ; :: thesis: ex p, g being Real st X = ].p,g.[
take p = lower_bound X; :: thesis: ex g being Real st X = ].p,g.[
take g = upper_bound X; :: thesis: X = ].p,g.[
now :: thesis: for r being Element of REAL holds
( ( r in X implies r in ].p,g.[ ) & ( r in ].p,g.[ implies r in X ) )
let r be Element of 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 ( p <> r & p <= r ) by A1, A2, Th22, SEQ_4:def 2;
then A7: p < r by XXREAL_0:1;
( g <> r & r <= g ) by A1, A2, A6, Th21, SEQ_4:def 1;
then r < g by XXREAL_0:1;
hence r in ].p,g.[ by A7; :: thesis: verum
end;
assume r in ].p,g.[ ; :: thesis: r in X
then A8: ex s being Real st
( s = r & p < s & s < g ) ;
then g - r > 0 by XREAL_1:50;
then consider g2 being Real such that
A9: ( g2 in X & g - (g - r) < g2 ) by A2, A5, SEQ_4:def 1;
r - p > 0 by A8, XREAL_1:50;
then consider g1 being Real such that
A10: ( g1 in X & g1 < p + (r - p) ) by A2, A5, SEQ_4:def 2;
reconsider g1 = g1, g2 = g2 as Real ;
( r in { s where s is Real : ( g1 <= s & s <= g2 ) } & [.g1,g2.] c= X ) by A3, A9, A10;
hence r in X ; :: thesis: verum
end;
hence X = ].p,g.[ by SUBSET_1:3; :: thesis: verum
end;
end;