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

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