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 object 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:52;
then (UMP C) `2 <= |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `2 by Th39;
then A3: x `2 >= (UMP C) `2 by A1, TOPREAL1:4;
|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| `2 = S-bound C by EUCLID:52;
then |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| `2 <= (LMP C) `2 by Th40;
then x `2 <= (LMP C) `2 by A2, TOPREAL1:4;
hence contradiction by A3, Th36, XXREAL_0:2; :: thesis: verum