let D be compact with_the_max_arc Subset of (TOP-REAL 2); :: thesis: LMP D in D
set w = ((W-bound D) + (E-bound D)) / 2;
set X = D /\ (Vertical_Line (((W-bound D) + (E-bound D)) / 2));
A1: proj2 .: (D /\ (Vertical_Line (((W-bound D) + (E-bound D)) / 2))) is bounded_below by Th13;
( not proj2 .: (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 ) by Th12, Th13;
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: lower_bound (proj2 .: (D /\ (Vertical_Line (((W-bound D) + (E-bound D)) / 2)))) = proj2 . x by A1, Lm2, RCOMP_1:31;
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
.= (LMP D) `1 by EUCLID:56 ;
x `2 = lower_bound (proj2 .: (D /\ (Vertical_Line (((W-bound D) + (E-bound D)) / 2)))) by A3, PSCOMP_1:def 29
.= (LMP D) `2 by EUCLID:56 ;
then x = LMP D by A4, TOPREAL3:11;
hence LMP D in D by A2, XBOOLE_0:def 4; :: thesis: verum