let D be compact with_the_max_arc Subset of (TOP-REAL 2); (LSeg ((LMP D),|[(((W-bound D) + (E-bound D)) / 2),(S-bound D)]|)) /\ D = {(LMP D)}
set C = D;
set w = ((W-bound D) + (E-bound D)) / 2;
set L = LSeg ((LMP D),|[(((W-bound D) + (E-bound D)) / 2),(S-bound D)]|);
set X = D /\ (Vertical_Line (((W-bound D) + (E-bound D)) / 2));
A1:
LMP D in D
by Th31;
A2:
LMP D in LSeg ((LMP D),|[(((W-bound D) + (E-bound D)) / 2),(S-bound D)]|)
by RLTOPSP1:68;
hereby TARSKI:def 3,
XBOOLE_0:def 10 {(LMP D)} c= (LSeg ((LMP D),|[(((W-bound D) + (E-bound D)) / 2),(S-bound D)]|)) /\ D
let x be
object ;
( x in (LSeg ((LMP D),|[(((W-bound D) + (E-bound D)) / 2),(S-bound D)]|)) /\ D implies x in {(LMP D)} )A3:
(LMP D) `1 = ((W-bound D) + (E-bound D)) / 2
by EUCLID:52;
assume A4:
x in (LSeg ((LMP D),|[(((W-bound D) + (E-bound D)) / 2),(S-bound D)]|)) /\ D
;
x in {(LMP D)}then A5:
x in LSeg (
(LMP D),
|[(((W-bound D) + (E-bound D)) / 2),(S-bound D)]|)
by XBOOLE_0:def 4;
reconsider y =
x as
Point of
(TOP-REAL 2) by A4;
LMP D in D
by Th31;
then
(
|[(((W-bound D) + (E-bound D)) / 2),(S-bound D)]| `2 = S-bound D &
(LMP D) `2 >= S-bound D )
by EUCLID:52, PSCOMP_1:24;
then A6:
(LMP D) `2 >= y `2
by A5, TOPREAL1:4;
A7:
proj2 .: (D /\ (Vertical_Line (((W-bound D) + (E-bound D)) / 2))) is
bounded_below
by Th13;
A8:
(LMP D) `2 = lower_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 (
(LMP D),
|[(((W-bound D) + (E-bound D)) / 2),(S-bound D)]|) is
vertical
by Th33;
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 >= lower_bound (proj2 .: (D /\ (Vertical_Line (((W-bound D) + (E-bound D)) / 2))))
by A7, SEQ_4:def 2;
then
y `2 = lower_bound (proj2 .: (D /\ (Vertical_Line (((W-bound D) + (E-bound D)) / 2))))
by A8, A6, XXREAL_0:1;
then
y = LMP D
by A3, A8, A10, TOPREAL3:6;
hence
x in {(LMP D)}
by TARSKI:def 1;
verum
end;
let x be object ; TARSKI:def 3 ( not x in {(LMP D)} or x in (LSeg ((LMP D),|[(((W-bound D) + (E-bound D)) / 2),(S-bound D)]|)) /\ D )
assume
x in {(LMP D)}
; x in (LSeg ((LMP D),|[(((W-bound D) + (E-bound D)) / 2),(S-bound D)]|)) /\ D
then
x = LMP D
by TARSKI:def 1;
hence
x in (LSeg ((LMP D),|[(((W-bound D) + (E-bound D)) / 2),(S-bound D)]|)) /\ D
by A2, A1, XBOOLE_0:def 4; verum