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]|,(UMP D)) /\ D = {(UMP D)} )
assume A1:
|[(- 1),0 ]|,|[1,0 ]| realize-max-dist-in D
; :: thesis: (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, Lm81;
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)}
:: according to XBOOLE_0:def 10 :: thesis: {(UMP D)} c= (LSeg |[0 ,3]|,(UMP D)) /\ Dproof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in (LSeg |[0 ,3]|,(UMP D)) /\ D or x in {(UMP D)} )
assume A6:
x in (LSeg |[0 ,3]|,(UMP D)) /\ D
;
:: thesis: x in {(UMP D)}
then A7:
(
x in LSeg |[0 ,3]|,
(UMP D) &
x in D )
by 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 A8:
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 A7, XBOOLE_0:def 4;
then A9:
x `2 <= (UMP D) `2
by JORDAN21:41;
(UMP D) `2 <= x `2
by A1, A7, Th85;
then
x `2 = (UMP D) `2
by A9, XXREAL_0:1;
then
x = UMP D
by A8, TOPREAL3:11;
hence
x in {(UMP D)}
by TARSKI:def 1;
:: thesis: verum
end;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {(UMP D)} or x in (LSeg |[0 ,3]|,(UMP D)) /\ D )
assume
x in {(UMP D)}
; :: thesis: 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; :: thesis: verum