let D be compact with_the_max_arc Subset of (TOP-REAL 2); ( |[(- 1),0 ]|,|[1,0 ]| realize-max-dist-in D implies (LSeg |[0 ,3]|,(UMP D)) /\ D = {(UMP D)} )
assume A1:
|[(- 1),0 ]|,|[1,0 ]| realize-max-dist-in D
; (LSeg |[0 ,3]|,(UMP D)) /\ D = {(UMP D)}
set m = UMP D;
set w = ((W-bound D) + (E-bound D)) / 2;
A2:
|[0 ,3]| `1 = ((W-bound D) + (E-bound D)) / 2
by A1, Lm87;
A3:
(UMP D) `1 = ((W-bound D) + (E-bound D)) / 2
by EUCLID:56;
A4:
UMP D in LSeg |[0 ,3]|,(UMP D)
by RLTOPSP1:69;
A5:
UMP D in D
by JORDAN21:43;
thus
(LSeg |[0 ,3]|,(UMP D)) /\ D c= {(UMP D)}
XBOOLE_0:def 10 {(UMP D)} c= (LSeg |[0 ,3]|,(UMP D)) /\ Dproof
let x be
set ;
TARSKI:def 3 ( not x in (LSeg |[0 ,3]|,(UMP D)) /\ D or x in {(UMP D)} )
assume A6:
x in (LSeg |[0 ,3]|,(UMP D)) /\ D
;
x in {(UMP D)}
then A7:
x in LSeg |[0 ,3]|,
(UMP 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]|,
(UMP D) is
vertical
by A2, A3, SPPOL_1:37;
then A9:
x `1 = (UMP 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 A8, XBOOLE_0:def 4;
then A10:
x `2 <= (UMP D) `2
by JORDAN21:41;
(UMP D) `2 <= x `2
by A1, A7, Th85;
then
x `2 = (UMP D) `2
by A10, XXREAL_0:1;
then
x = UMP D
by A9, TOPREAL3:11;
hence
x in {(UMP D)}
by TARSKI:def 1;
verum
end;
let x be set ; TARSKI:def 3 ( not x in {(UMP D)} or x in (LSeg |[0 ,3]|,(UMP D)) /\ D )
assume
x in {(UMP D)}
; x in (LSeg |[0 ,3]|,(UMP D)) /\ D
then
x = UMP D
by TARSKI:def 1;
hence
x in (LSeg |[0 ,3]|,(UMP D)) /\ D
by A4, A5, XBOOLE_0:def 4; verum