let P be non empty Subset of (TOP-REAL 2); :: thesis: ( P is being_simple_closed_curve iff ex p1, p2 being Point of (TOP-REAL 2) ex P1, P2 being non empty Subset of (TOP-REAL 2) st
( p1 <> p2 & p1 in P & p2 in P & P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P = P1 \/ P2 & P1 /\ P2 = {p1,p2} ) )

hereby :: thesis: ( ex p1, p2 being Point of (TOP-REAL 2) ex P1, P2 being non empty Subset of (TOP-REAL 2) st
( p1 <> p2 & p1 in P & p2 in P & P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P = P1 \/ P2 & P1 /\ P2 = {p1,p2} ) implies P is being_simple_closed_curve )

assume A1: P is being_simple_closed_curve ; :: thesis: ex p1, p2 being Point of (TOP-REAL 2) ex P1, P2 being non empty Subset of (TOP-REAL 2) st
( p1 <> p2 & p1 in P & p2 in P & P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
then consider p1, p2 being Point of (TOP-REAL 2) such that
A2: p1 <> p2 and
A3: p1 in P and
A4: p2 in P by Th5;
consider P1, P2 being non empty Subset of (TOP-REAL 2) such that
A5: P1 is_an_arc_of p1,p2 and
A6: P2 is_an_arc_of p1,p2 and
A7: P = P1 \/ P2 and
A8: P1 /\ P2 = {p1,p2} by A1, A2, A3, A4, Th5;
take p1 = p1; :: thesis: ex p2 being Point of (TOP-REAL 2) ex P1, P2 being non empty Subset of (TOP-REAL 2) st
( p1 <> p2 & p1 in P & p2 in P & P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
take p2 = p2; :: thesis: ex P1, P2 being non empty Subset of (TOP-REAL 2) st
( p1 <> p2 & p1 in P & p2 in P & P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
take P1 = P1; :: thesis: ex P2 being non empty Subset of (TOP-REAL 2) st
( p1 <> p2 & p1 in P & p2 in P & P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
take P2 = P2; :: thesis: ( p1 <> p2 & p1 in P & p2 in P & P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
thus ( p1 <> p2 & p1 in P & p2 in P & P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P = P1 \/ P2 & P1 /\ P2 = {p1,p2} ) by A2, A3, A4, A5, A6, A7, A8; :: thesis: verum

end;

thus ( ex p1, p2 being Point of (TOP-REAL 2) ex P1, P2 being non empty Subset of (TOP-REAL 2) st
( p1 <> p2 & p1 in P & p2 in P & P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P = P1 \/ P2 & P1 /\ P2 = {p1,p2} ) implies P is being_simple_closed_curve ) by Lm34; :: thesis: verum