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.]

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

now

let r be 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 4, SEQ_4:def 5;
hence r in [.p,g.] ; :: thesis: verum

end;

then A6: X c= [.p,g.] by SUBSET_1:7;
( upper_bound X in X & lower_bound X in X ) by A4, A5, Th30, Th31;
then [.p,g.] c= X by A2;
hence X = [.p,g.] by A6, XBOOLE_0:def 10; :: thesis: verum

end;

end;