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