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 Th44;
A2: LMP D in LSeg (LMP D),|[(((W-bound D) + (E-bound D)) / 2),(S-bound D)]| by RLTOPSP1:69;

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 set ; :: 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:56;
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 Th44;
then ( |[(((W-bound D) + (E-bound D)) / 2),(S-bound D)]| `2 = S-bound D & (LMP D) `2 >= S-bound D ) by EUCLID:56, PSCOMP_1:71;
then A6: (LMP D) `2 >= y `2 by A5, TOPREAL1:10;
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:56;
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 Th46;
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:34;
then ( y `2 = proj2 . y & y in D /\ (Vertical_Line (((W-bound D) + (E-bound D)) / 2)) ) by A9, PSCOMP_1:def 29, XBOOLE_0:def 4;
then y `2 in proj2 .: (D /\ (Vertical_Line (((W-bound D) + (E-bound D)) / 2))) by FUNCT_2:43;
then y `2 >= lower_bound (proj2 .: (D /\ (Vertical_Line (((W-bound D) + (E-bound D)) / 2)))) by A7, SEQ_4:def 5;
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:11;
hence x in {(LMP D)} by TARSKI:def 1; :: thesis: verum

end;

let x be set ; :: 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