let P be Subset of (TOP-REAL 2); :: thesis: ( P is being_special_polygon implies P is being_simple_closed_curve )

given p1, p2 being Point of (TOP-REAL 2), P1, P2 being Subset of (TOP-REAL 2) such that A1: ( p1 <> p2 & p1 in P & p2 in P ) and

A2: ( P1 is_S-P_arc_joining p1,p2 & P2 is_S-P_arc_joining p1,p2 ) and

A3: P1 /\ P2 = {p1,p2} and

A4: P = P1 \/ P2 ; :: according to TOPREAL4:def 2 :: thesis: P is being_simple_closed_curve

reconsider P1 = P1, P2 = P2 as non empty Subset of (TOP-REAL 2) by A3;

( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 ) by A2, Th2;

hence P is being_simple_closed_curve by A1, A3, A4, TOPREAL2:6; :: thesis: verum

given p1, p2 being Point of (TOP-REAL 2), P1, P2 being Subset of (TOP-REAL 2) such that A1: ( p1 <> p2 & p1 in P & p2 in P ) and

A2: ( P1 is_S-P_arc_joining p1,p2 & P2 is_S-P_arc_joining p1,p2 ) and

A3: P1 /\ P2 = {p1,p2} and

A4: P = P1 \/ P2 ; :: according to TOPREAL4:def 2 :: thesis: P is being_simple_closed_curve

reconsider P1 = P1, P2 = P2 as non empty Subset of (TOP-REAL 2) by A3;

( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 ) by A2, Th2;

hence P is being_simple_closed_curve by A1, A3, A4, TOPREAL2:6; :: thesis: verum