let P be Subset of (); :: thesis: ( P is special_polygonal implies for p1, p2 being Point of () st p1 <> p2 & p1 in P & p2 in P holds
ex P1, P2 being Subset of () st
( P1 is_S-P_arc_joining p1,p2 & P2 is_S-P_arc_joining p1,p2 & P1 /\ P2 = {p1,p2} & P = P1 \/ P2 ) )

assume A1: P is special_polygonal ; :: thesis: for p1, p2 being Point of () st p1 <> p2 & p1 in P & p2 in P holds
ex P1, P2 being Subset of () st
( P1 is_S-P_arc_joining p1,p2 & P2 is_S-P_arc_joining p1,p2 & P1 /\ P2 = {p1,p2} & P = P1 \/ P2 )

let p1, p2 be Point of (); :: thesis: ( p1 <> p2 & p1 in P & p2 in P implies ex P1, P2 being Subset of () st
( P1 is_S-P_arc_joining p1,p2 & P2 is_S-P_arc_joining p1,p2 & P1 /\ P2 = {p1,p2} & P = P1 \/ P2 ) )

assume that
A2: p1 <> p2 and
A3: p1 in P and
A4: p2 in P ; :: thesis: ex P1, P2 being Subset of () st
( P1 is_S-P_arc_joining p1,p2 & P2 is_S-P_arc_joining p1,p2 & P1 /\ P2 = {p1,p2} & P = P1 \/ P2 )

p1,p2 split P by A1, A2, A3, A4, Th58;
then consider f1, f2 being S-Sequence_in_R2 such that
A5: p1 = f1 /. 1 and
A6: p1 = f2 /. 1 and
A7: p2 = f1 /. (len f1) and
A8: p2 = f2 /. (len f2) and
A9: (L~ f1) /\ (L~ f2) = {p1,p2} and
A10: P = (L~ f1) \/ (L~ f2) ;
take P1 = L~ f1; :: thesis: ex P2 being Subset of () st
( P1 is_S-P_arc_joining p1,p2 & P2 is_S-P_arc_joining p1,p2 & P1 /\ P2 = {p1,p2} & P = P1 \/ P2 )

take P2 = L~ f2; :: thesis: ( P1 is_S-P_arc_joining p1,p2 & P2 is_S-P_arc_joining p1,p2 & P1 /\ P2 = {p1,p2} & P = P1 \/ P2 )
thus P1 is_S-P_arc_joining p1,p2 by A5, A7; :: thesis: ( P2 is_S-P_arc_joining p1,p2 & P1 /\ P2 = {p1,p2} & P = P1 \/ P2 )
thus P2 is_S-P_arc_joining p1,p2 by A6, A8; :: thesis: ( P1 /\ P2 = {p1,p2} & P = P1 \/ P2 )
thus ( P1 /\ P2 = {p1,p2} & P = P1 \/ P2 ) by ; :: thesis: verum