let C be Simple_closed_curve; :: thesis: LSeg (UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| misses LSeg (LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|
set w = ((W-bound C) + (E-bound C)) / 2;
assume LSeg (UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| meets LSeg (LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| ; :: thesis: contradiction
then consider x being set such that
A1: x in LSeg (UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| and
A2: x in LSeg (LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| by XBOOLE_0:3;
reconsider x = x as Point of (TOP-REAL 2) by A1;
|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `2 = N-bound C by EUCLID:56;
then (UMP C) `2 <= |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `2 by Th52;
then A3: x `2 >= (UMP C) `2 by A1, TOPREAL1:10;
|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| `2 = S-bound C by EUCLID:56;
then |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| `2 <= (LMP C) `2 by Th53;
then x `2 <= (LMP C) `2 by A2, TOPREAL1:10;
hence contradiction by A3, Th49, XXREAL_0:2; :: thesis: verum