let P be non empty Subset of (); :: thesis: ( P is being_simple_closed_curve iff ex p1, p2 being Point of () ex P1, P2 being non empty Subset of () 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 () ex P1, P2 being non empty Subset of () 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 () ex P1, P2 being non empty Subset of () 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 () 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 () 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 () ex P1, P2 being non empty Subset of () 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 () 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 () 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 () ex P1, P2 being non empty Subset of () 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