let D be compact with_the_max_arc Subset of (TOP-REAL 2); (LSeg (UMP D),|[(((W-bound D) + (E-bound D)) / 2),(N-bound D)]|) /\ D = {(UMP D)}
set C = D;
set w = ((W-bound D) + (E-bound D)) / 2;
set L = LSeg (UMP D),|[(((W-bound D) + (E-bound D)) / 2),(N-bound D)]|;
set X = D /\ (Vertical_Line (((W-bound D) + (E-bound D)) / 2));
A1:
UMP D in D
by Th43;
A2:
UMP D in LSeg (UMP D),|[(((W-bound D) + (E-bound D)) / 2),(N-bound D)]|
by RLTOPSP1:69;
hereby TARSKI:def 3,
XBOOLE_0:def 10 {(UMP D)} c= (LSeg (UMP D),|[(((W-bound D) + (E-bound D)) / 2),(N-bound D)]|) /\ D
let x be
set ;
( x in (LSeg (UMP D),|[(((W-bound D) + (E-bound D)) / 2),(N-bound D)]|) /\ D implies x in {(UMP D)} )A3:
(UMP D) `1 = ((W-bound D) + (E-bound D)) / 2
by EUCLID:56;
assume A4:
x in (LSeg (UMP D),|[(((W-bound D) + (E-bound D)) / 2),(N-bound D)]|) /\ D
;
x in {(UMP D)}then A5:
x in LSeg (UMP D),
|[(((W-bound D) + (E-bound D)) / 2),(N-bound D)]|
by XBOOLE_0:def 4;
reconsider y =
x as
Point of
(TOP-REAL 2) by A4;
UMP D in D
by Th43;
then
(
|[(((W-bound D) + (E-bound D)) / 2),(N-bound D)]| `2 = N-bound D &
(UMP D) `2 <= N-bound D )
by EUCLID:56, PSCOMP_1:71;
then A6:
(UMP D) `2 <= y `2
by A5, TOPREAL1:10;
A7:
proj2 .: (D /\ (Vertical_Line (((W-bound D) + (E-bound D)) / 2))) is
bounded_above
by Th13;
A8:
(UMP D) `2 = upper_bound (proj2 .: (D /\ (Vertical_Line (((W-bound D) + (E-bound D)) / 2))))
by EUCLID:56;
A9:
x in D
by A4, XBOOLE_0:def 4;
LSeg (UMP D),
|[(((W-bound D) + (E-bound D)) / 2),(N-bound D)]| is
vertical
by Th45;
then A10:
y `1 = ((W-bound D) + (E-bound D)) / 2
by A2, A5, A3, SPPOL_1:def 3;
then
y in Vertical_Line (((W-bound D) + (E-bound D)) / 2)
by JORDAN6:34;
then
(
y `2 = proj2 . y &
y in D /\ (Vertical_Line (((W-bound D) + (E-bound D)) / 2)) )
by A9, PSCOMP_1:def 29, XBOOLE_0:def 4;
then
y `2 in proj2 .: (D /\ (Vertical_Line (((W-bound D) + (E-bound D)) / 2)))
by FUNCT_2:43;
then
y `2 <= upper_bound (proj2 .: (D /\ (Vertical_Line (((W-bound D) + (E-bound D)) / 2))))
by A7, SEQ_4:def 4;
then
y `2 = upper_bound (proj2 .: (D /\ (Vertical_Line (((W-bound D) + (E-bound D)) / 2))))
by A8, A6, XXREAL_0:1;
then
y = UMP D
by A3, A8, A10, 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 (UMP D),|[(((W-bound D) + (E-bound D)) / 2),(N-bound D)]|) /\ D )
assume
x in {(UMP D)}
; x in (LSeg (UMP D),|[(((W-bound D) + (E-bound D)) / 2),(N-bound D)]|) /\ D
then
x = UMP D
by TARSKI:def 1;
hence
x in (LSeg (UMP D),|[(((W-bound D) + (E-bound D)) / 2),(N-bound D)]|) /\ D
by A2, A1, XBOOLE_0:def 4; verum