let C be Simple_closed_curve; :: thesis: Lower_Arc C <> Upper_Arc C
assume Lower_Arc C = Upper_Arc C ; :: thesis: contradiction
then A1: Lower_Arc C = (C \ (Lower_Arc C)) \/ {(W-min C),(E-max C)} by JORDAN6:51;
Lower_Arc C is_an_arc_of W-min C, E-max C by JORDAN6:50;
then A2: ex p3 being Point of (TOP-REAL 2) st
( p3 in Lower_Arc C & p3 <> W-min C & p3 <> E-max C ) by JORDAN6:42;
Lower_Arc C misses C \ (Lower_Arc C) by XBOOLE_1:79;
then Lower_Arc C c= {(W-min C),(E-max C)} by A1, XBOOLE_1:73;
hence contradiction by A2, TARSKI:def 2; :: thesis: verum