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:52;
A4:
UMP D in LSeg (|[0,3]|,(UMP D))
by RLTOPSP1:68;
A5:
UMP D in D
by JORDAN21:30;
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
object ;
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:16;
then A9:
x `1 = (UMP 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:
x `2 <= (UMP D) `2
by JORDAN21:28;
(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:6;
hence
x in {(UMP D)}
by TARSKI:def 1;
verum
end;
let x be object ; 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