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 Th30;
A2:
UMP D in LSeg ((UMP D),|[(((W-bound D) + (E-bound D)) / 2),(N-bound D)]|)
by RLTOPSP1:68;
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
object ;
( 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:52;
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 Th30;
then
(
|[(((W-bound D) + (E-bound D)) / 2),(N-bound D)]| `2 = N-bound D &
(UMP D) `2 <= N-bound D )
by EUCLID:52, PSCOMP_1:24;
then A6:
(UMP D) `2 <= y `2
by A5, TOPREAL1:4;
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:52;
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 Th32;
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:31;
then
(
y `2 = proj2 . y &
y in D /\ (Vertical_Line (((W-bound D) + (E-bound D)) / 2)) )
by A9, PSCOMP_1:def 6, XBOOLE_0:def 4;
then
y `2 in proj2 .: (D /\ (Vertical_Line (((W-bound D) + (E-bound D)) / 2)))
by FUNCT_2:35;
then
y `2 <= upper_bound (proj2 .: (D /\ (Vertical_Line (((W-bound D) + (E-bound D)) / 2))))
by A7, SEQ_4:def 1;
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: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 ((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