let C be Simple_closed_curve; :: thesis: for p being Point of (TOP-REAL 2) st p `1 = ((W-bound C) + (E-bound C)) / 2 & p in North_Arc C holds
not p in South_Arc C
let p be Point of (TOP-REAL 2); :: thesis: ( p `1 = ((W-bound C) + (E-bound C)) / 2 & p in North_Arc C implies not p in South_Arc C )
A1: W-bound C < E-bound C by SPRECT_1:31;
assume A2: p `1 = ((W-bound C) + (E-bound C)) / 2 ; :: thesis: ( not p in North_Arc C or not p in South_Arc C )
then A3: W-bound C < p `1 by A1, XREAL_1:226;
p `1 < E-bound C by A1, A2, XREAL_1:226;
hence ( not p in North_Arc C or not p in South_Arc C ) by A3, Th26; :: thesis: verum