let D be compact with_the_max_arc Subset of (TOP-REAL 2); :: thesis: (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 LSeg (UMP D),|[(((W-bound D) + (E-bound D)) / 2),(N-bound D)]|
by RLTOPSP1:69;
hereby :: according to TARSKI:def 3,
XBOOLE_0:def 10 :: thesis: {(UMP D)} c= (LSeg (UMP D),|[(((W-bound D) + (E-bound D)) / 2),(N-bound D)]|) /\ D
let x be
set ;
:: thesis: ( x in (LSeg (UMP D),|[(((W-bound D) + (E-bound D)) / 2),(N-bound D)]|) /\ D implies x in {(UMP D)} )assume A2:
x in (LSeg (UMP D),|[(((W-bound D) + (E-bound D)) / 2),(N-bound D)]|) /\ D
;
:: thesis: x in {(UMP D)}then A3:
(
x in LSeg (UMP D),
|[(((W-bound D) + (E-bound D)) / 2),(N-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),(N-bound D)]| `2 = N-bound D
by EUCLID:56;
A5:
(UMP D) `1 = ((W-bound D) + (E-bound D)) / 2
by EUCLID:56;
A6:
(UMP D) `2 = sup (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_above
by Th13;
LSeg (UMP D),
|[(((W-bound D) + (E-bound D)) / 2),(N-bound D)]| is
vertical
by Th45;
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 <= sup (proj2 .: (D /\ (Vertical_Line (((W-bound D) + (E-bound D)) / 2))))
by A7, SEQ_4:def 4;
UMP D in D
by Th43;
then
(UMP D) `2 <= N-bound D
by PSCOMP_1:71;
then
(UMP D) `2 <= y `2
by A3, A4, TOPREAL1:10;
then
y `2 = sup (proj2 .: (D /\ (Vertical_Line (((W-bound D) + (E-bound D)) / 2))))
by A6, A10, XXREAL_0:1;
then
y = UMP D
by A5, A6, 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 (UMP D),|[(((W-bound D) + (E-bound D)) / 2),(N-bound D)]|) /\ D )
assume
x in {(UMP D)}
; :: thesis: x in (LSeg (UMP D),|[(((W-bound D) + (E-bound D)) / 2),(N-bound D)]|) /\ D
then A11:
x = UMP D
by TARSKI:def 1;
UMP D in D
by Th43;
hence
x in (LSeg (UMP D),|[(((W-bound D) + (E-bound D)) / 2),(N-bound D)]|) /\ D
by A1, A11, XBOOLE_0:def 4; :: thesis: verum