let D be compact with_the_max_arc Subset of (TOP-REAL 2); :: thesis: UMP D in D
set w = ((W-bound D) + (E-bound D)) / 2;
set X = D /\ (Vertical_Line (((W-bound D) + (E-bound D)) / 2));
D meets Vertical_Line (((W-bound D) + (E-bound D)) / 2) by Def1;
then A1: not D /\ (Vertical_Line (((W-bound D) + (E-bound D)) / 2)) is empty by XBOOLE_0:def 7;
( proj2 .: (D /\ (Vertical_Line (((W-bound D) + (E-bound D)) / 2))) is closed & proj2 .: (D /\ (Vertical_Line (((W-bound D) + (E-bound D)) / 2))) is bounded_above ) by Th13;
then upper_bound (proj2 .: (D /\ (Vertical_Line (((W-bound D) + (E-bound D)) / 2)))) in proj2 .: (D /\ (Vertical_Line (((W-bound D) + (E-bound D)) / 2))) by A1, Lm1, RCOMP_1:30, RELAT_1:152;
then consider x being Point of (TOP-REAL 2) such that
A2: x in D /\ (Vertical_Line (((W-bound D) + (E-bound D)) / 2)) and
A3: upper_bound (proj2 .: (D /\ (Vertical_Line (((W-bound D) + (E-bound D)) / 2)))) = proj2 . x by Lm2;
x in Vertical_Line (((W-bound D) + (E-bound D)) / 2) by A2, XBOOLE_0:def 4;
then A4: x `1 = ((W-bound D) + (E-bound D)) / 2 by JORDAN6:34
.= (UMP D) `1 by EUCLID:56 ;
x `2 = upper_bound (proj2 .: (D /\ (Vertical_Line (((W-bound D) + (E-bound D)) / 2)))) by A3, PSCOMP_1:def 29
.= (UMP D) `2 by EUCLID:56 ;
then x = UMP D by A4, TOPREAL3:11;
hence UMP D in D by A2, XBOOLE_0:def 4; :: thesis: verum