theorem Th35: :: JORDAN21:35

for D being compact with_the_max_arc Subset of (TOP-REAL 2) holds (LSeg ((LMP D),|[(((W-bound D) + (E-bound D)) / 2),(S-bound D)]|)) /\ D = {(LMP D)}