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 D by Th30;
A2: UMP D in LSeg ((UMP D),|[(((W-bound D) + (E-bound D)) / 2),(N-bound D)]|) by RLTOPSP1:68;

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 object ; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum

end;

let x be object ; :: 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 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; :: thesis: verum