let D be compact with_the_max_arc Subset of (TOP-REAL 2); :: thesis: (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 LSeg (LMP D),|[(((W-bound D) + (E-bound D)) / 2),(S-bound D)]|
by RLTOPSP1:69;
hereby :: according to TARSKI:def 3,
XBOOLE_0:def 10 :: thesis: {(LMP D)} c= (LSeg (LMP D),|[(((W-bound D) + (E-bound D)) / 2),(S-bound D)]|) /\ D
let x be
set ;
:: thesis: ( x in (LSeg (LMP D),|[(((W-bound D) + (E-bound D)) / 2),(S-bound D)]|) /\ D implies x in {(LMP D)} )assume A2:
x in (LSeg (LMP D),|[(((W-bound D) + (E-bound D)) / 2),(S-bound D)]|) /\ D
;
:: thesis: x in {(LMP D)}then A3:
(
x in LSeg (LMP D),
|[(((W-bound D) + (E-bound D)) / 2),(S-bound D)]| &
x in D )
by XBOOLE_0:def 4;
reconsider y =
x as
Point of
(TOP-REAL 2) by A2;
A4:
|[(((W-bound D) + (E-bound D)) / 2),(S-bound D)]| `2 = S-bound D
by EUCLID:56;
A5:
(LMP D) `1 = ((W-bound D) + (E-bound D)) / 2
by EUCLID:56;
A6:
(LMP D) `2 = inf (proj2 .: (D /\ (Vertical_Line (((W-bound D) + (E-bound D)) / 2))))
by EUCLID:56;
A7:
proj2 .: (D /\ (Vertical_Line (((W-bound D) + (E-bound D)) / 2))) is
bounded_below
by Th13;
LSeg (LMP D),
|[(((W-bound D) + (E-bound D)) / 2),(S-bound D)]| is
vertical
by Th46;
then A8:
y `1 = ((W-bound D) + (E-bound D)) / 2
by A1, A3, A5, SPPOL_1:def 3;
A9:
y `2 = proj2 . y
by PSCOMP_1:def 29;
y in Vertical_Line (((W-bound D) + (E-bound D)) / 2)
by A8, JORDAN6:34;
then
y in D /\ (Vertical_Line (((W-bound D) + (E-bound D)) / 2))
by A3, XBOOLE_0:def 4;
then
y `2 in proj2 .: (D /\ (Vertical_Line (((W-bound D) + (E-bound D)) / 2)))
by A9, FUNCT_2:43;
then A10:
y `2 >= inf (proj2 .: (D /\ (Vertical_Line (((W-bound D) + (E-bound D)) / 2))))
by A7, SEQ_4:def 5;
LMP D in D
by Th44;
then
(LMP D) `2 >= S-bound D
by PSCOMP_1:71;
then
(LMP D) `2 >= y `2
by A3, A4, TOPREAL1:10;
then
y `2 = inf (proj2 .: (D /\ (Vertical_Line (((W-bound D) + (E-bound D)) / 2))))
by A6, A10, XXREAL_0:1;
then
y = LMP D
by A5, A6, A8, TOPREAL3:11;
hence
x in {(LMP D)}
by TARSKI:def 1;
:: thesis: verum
end;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( 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)}
; :: thesis: x in (LSeg (LMP D),|[(((W-bound D) + (E-bound D)) / 2),(S-bound D)]|) /\ D
then A11:
x = LMP D
by TARSKI:def 1;
LMP D in D
by Th44;
hence
x in (LSeg (LMP D),|[(((W-bound D) + (E-bound D)) / 2),(S-bound D)]|) /\ D
by A1, A11, XBOOLE_0:def 4; :: thesis: verum