let D be compact with_the_max_arc Subset of (TOP-REAL 2); :: thesis: (LSeg ((LMP D),|[(((W-bound D) + (E-bound D)) / 2),(S-bound D)]|)) /\ D = {(LMP D)}
set C = D;
set w = ((W-bound D) + (E-bound D)) / 2;
set L = LSeg ((LMP D),|[(((W-bound D) + (E-bound D)) / 2),(S-bound D)]|);
set X = D /\ (Vertical_Line (((W-bound D) + (E-bound D)) / 2));
A1: LMP D in D by Th31;
A2: LMP D in LSeg ((LMP D),|[(((W-bound D) + (E-bound D)) / 2),(S-bound D)]|) by RLTOPSP1:68;

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: {(LMP D)} c= (LSeg ((LMP D),|[(((W-bound D) + (E-bound D)) / 2),(S-bound D)]|)) /\ D

let x be object ; :: thesis: ( x in (LSeg ((LMP D),|[(((W-bound D) + (E-bound D)) / 2),(S-bound D)]|)) /\ D implies x in {(LMP D)} )
A3: (LMP D) `1 = ((W-bound D) + (E-bound D)) / 2 by EUCLID:52;
assume A4: x in (LSeg ((LMP D),|[(((W-bound D) + (E-bound D)) / 2),(S-bound D)]|)) /\ D ; :: thesis: x in {(LMP D)}
then A5: x in LSeg ((LMP D),|[(((W-bound D) + (E-bound D)) / 2),(S-bound D)]|) by XBOOLE_0:def 4;
reconsider y = x as Point of (TOP-REAL 2) by A4;
LMP D in D by Th31;
then ( |[(((W-bound D) + (E-bound D)) / 2),(S-bound D)]| `2 = S-bound D & (LMP D) `2 >= S-bound D ) by EUCLID:52, PSCOMP_1:24;
then A6: (LMP D) `2 >= y `2 by A5, TOPREAL1:4;
A7: proj2 .: (D /\ (Vertical_Line (((W-bound D) + (E-bound D)) / 2))) is bounded_below by Th13;
A8: (LMP D) `2 = lower_bound (proj2 .: (D /\ (Vertical_Line (((W-bound D) + (E-bound D)) / 2)))) by EUCLID:52;
A9: x in D by A4, XBOOLE_0:def 4;
LSeg ((LMP D),|[(((W-bound D) + (E-bound D)) / 2),(S-bound D)]|) is vertical by Th33;
then A10: y `1 = ((W-bound D) + (E-bound D)) / 2 by A2, A5, A3, SPPOL_1:def 3;
then y in Vertical_Line (((W-bound D) + (E-bound D)) / 2) by JORDAN6:31;
then ( y `2 = proj2 . y & y in D /\ (Vertical_Line (((W-bound D) + (E-bound D)) / 2)) ) by A9, PSCOMP_1:def 6, XBOOLE_0:def 4;
then y `2 in proj2 .: (D /\ (Vertical_Line (((W-bound D) + (E-bound D)) / 2))) by FUNCT_2:35;
then y `2 >= lower_bound (proj2 .: (D /\ (Vertical_Line (((W-bound D) + (E-bound D)) / 2)))) by A7, SEQ_4:def 2;
then y `2 = lower_bound (proj2 .: (D /\ (Vertical_Line (((W-bound D) + (E-bound D)) / 2)))) by A8, A6, XXREAL_0:1;
then y = LMP D by A3, A8, A10, TOPREAL3:6;
hence x in {(LMP D)} by TARSKI:def 1; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {(LMP D)} or x in (LSeg ((LMP D),|[(((W-bound D) + (E-bound D)) / 2),(S-bound D)]|)) /\ D )
assume x in {(LMP D)} ; :: thesis: x in (LSeg ((LMP D),|[(((W-bound D) + (E-bound D)) / 2),(S-bound D)]|)) /\ D
then x = LMP D by TARSKI:def 1;
hence x in (LSeg ((LMP D),|[(((W-bound D) + (E-bound D)) / 2),(S-bound D)]|)) /\ D by A2, A1, XBOOLE_0:def 4; :: thesis: verum