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, Lm82;
A3:
(LMP D) `1 = ((W-bound D) + (E-bound D)) / 2
by EUCLID:56;
A4:
LMP D in LSeg |[0 ,(- 3)]|,(LMP D)
by RLTOPSP1:69;
A5:
LMP D in D
by JORDAN21:44;
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)) /\ Dproof
let x be
set ;
:: 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) &
x in D )
by 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:37;
then A8:
x `1 = (LMP D) `1
by A4, A7, SPPOL_1:def 3;
then
x in Vertical_Line (((W-bound D) + (E-bound D)) / 2)
by A3, JORDAN6:34;
then
x in D /\ (Vertical_Line (((W-bound D) + (E-bound D)) / 2))
by A7, XBOOLE_0:def 4;
then A9:
(LMP D) `2 <= x `2
by JORDAN21:42;
x `2 <= (LMP D) `2
by A1, A7, Th86;
then
x `2 = (LMP D) `2
by A9, XXREAL_0:1;
then
x = LMP D
by A8, 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 |[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