let C be Simple_closed_curve; 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); ( 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
; ( 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; verum