let P be Simple_closed_curve; :: thesis: for a being Point of (TOP-REAL 2) st a in P holds
a,a,a,a are_in_this_order_on P
let a be Point of (TOP-REAL 2); :: thesis: ( a in P implies a,a,a,a are_in_this_order_on P )
assume a in P ; :: thesis: a,a,a,a are_in_this_order_on P
then LE a,a,P by JORDAN6:56;
hence a,a,a,a are_in_this_order_on P by Def1; :: thesis: verum