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} ) )

( 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

( 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 )

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 )

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;( 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

( 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