let X be Subset of REAL; :: thesis: ( X is compact & ( 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 compact and
A2: 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 A3: 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 A3, XXREAL_1:29; :: thesis: verum
end;
suppose A4: 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.]
A5: ( X is real-bounded & X is closed ) by A1, Th10;
now :: thesis: for r being Element of REAL st r in X holds
r in [.p,g.]
let r be Element of REAL ; :: thesis: ( r in X implies r in [.p,g.] )
assume r in X ; :: thesis: r in [.p,g.]
then ( r <= g & p <= r ) by A5, SEQ_4:def 1, SEQ_4:def 2;
hence r in [.p,g.] ; :: thesis: verum
end;
then A6: X c= [.p,g.] ;
( upper_bound X in X & lower_bound X in X ) by A4, A5, Th12, Th13;
then [.p,g.] c= X by A2;
hence X = [.p,g.] by A6; :: thesis: verum
end;
end;