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 ;
( 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:12, RELAT_1:119;
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:31
.= (UMP D) `1 by EUCLID:52 ;
x `2 = upper_bound (proj2 .: (D /\ (Vertical_Line (((W-bound D) + (E-bound D)) / 2)))) by A3, PSCOMP_1:def 6
.= (UMP D) `2 by EUCLID:52 ;
then x = UMP D by A4, TOPREAL3:6;
hence UMP D in D by A2, XBOOLE_0:def 4; :: thesis: verum