let X be Subset of REAL ; :: thesis: ( X is compact & ( 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 compact 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:29; :: thesis: verum

end;

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

( X is bounded & X is closed ) by A1, Th28;
then A5: ( X is bounded_below & X is bounded_above & X is closed ) ;
then A6: upper_bound X in X by A4, Th30;
A7: lower_bound X in X by A4, A5, Th31;
take p = lower_bound X; :: thesis: ex g being real number st X = [.p,g.]
take g = upper_bound X; :: thesis: X = [.p,g.]
A8: [.p,g.] c= X by A2, A6, A7;

now

let r be Real; :: thesis: ( r in X implies r in [.p,g.] )
assume A9: r in X ; :: thesis: r in [.p,g.]
then A10: r <= g by A5, SEQ_4:def 4;
p <= r by A5, A9, SEQ_4:def 5;
hence r in [.p,g.] by A10; :: thesis: verum

end;

then X c= [.p,g.] by SUBSET_1:7;
hence X = [.p,g.] by A8, XBOOLE_0:def 10; :: thesis: verum

end;

end;