let D be compact with_the_max_arc Subset of (TOP-REAL 2); :: thesis: ( |[(- 1),0]|,|[1,0]| realize-max-dist-in D implies (LSeg (|[0,(- 3)]|,(LMP D))) /\ D = {(LMP D)} )
assume A1: |[(- 1),0]|,|[1,0]| realize-max-dist-in D ; :: thesis: (LSeg (|[0,(- 3)]|,(LMP D))) /\ D = {(LMP D)}
set m = LMP D;
set w = ((W-bound D) + (E-bound D)) / 2;
A2: |[0,(- 3)]| `1 = ((W-bound D) + (E-bound D)) / 2 by A1, Lm88;
A3: (LMP D) `1 = ((W-bound D) + (E-bound D)) / 2 by EUCLID:52;
A4: LMP D in LSeg (|[0,(- 3)]|,(LMP D)) by RLTOPSP1:68;
A5: LMP D in D by JORDAN21:31;
thus (LSeg (|[0,(- 3)]|,(LMP D))) /\ D c= {(LMP D)} :: according to XBOOLE_0:def 10 :: thesis: {(LMP D)} c= (LSeg (|[0,(- 3)]|,(LMP D))) /\ D

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (LSeg (|[0,(- 3)]|,(LMP D))) /\ D or x in {(LMP D)} )
assume A6: x in (LSeg (|[0,(- 3)]|,(LMP D))) /\ D ; :: thesis: x in {(LMP D)}
then A7: x in LSeg (|[0,(- 3)]|,(LMP D)) by XBOOLE_0:def 4;
A8: x in D by A6, XBOOLE_0:def 4;
reconsider x = x as Point of (TOP-REAL 2) by A6;
LSeg (|[0,(- 3)]|,(LMP D)) is vertical by A2, A3, SPPOL_1:16;
then A9: x `1 = (LMP D) `1 by A4, A7;
then x in Vertical_Line (((W-bound D) + (E-bound D)) / 2) by A3, JORDAN6:31;
then x in D /\ (Vertical_Line (((W-bound D) + (E-bound D)) / 2)) by A8, XBOOLE_0:def 4;
then A10: (LMP D) `2 <= x `2 by JORDAN21:29;
x `2 <= (LMP D) `2 by A1, A7, Th86;
then x `2 = (LMP D) `2 by A10, XXREAL_0:1;
then x = LMP D by A9, 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 (|[0,(- 3)]|,(LMP D))) /\ D )
assume x in {(LMP D)} ; :: thesis: x in (LSeg (|[0,(- 3)]|,(LMP D))) /\ D
then x = LMP D by TARSKI:def 1;
hence x in (LSeg (|[0,(- 3)]|,(LMP D))) /\ D by A4, A5, XBOOLE_0:def 4; :: thesis: verum