let P be Subset of (TOP-REAL 2); :: thesis:
assume A1: P is special_polygonal ; :: thesis:
let p1, p2 be Point of (TOP-REAL 2); :: thesis:
assume ( p1 <> p2 & p1 in P & p2 in P ) ; :: thesis:
then p1,p2 split P by A1, Th64;
then consider f1, f2 being S-Sequence_in_R2 such that
A2: p1 = f1 /. 1 and
A3: p1 = f2 /. 1 and
A4: p2 = f1 /. (len f1) and
A5: p2 = f2 /. (len f2) and
A6: ( (L~ f1) /\ (L~ f2) = {p1,p2} & P = (L~ f1) \/ (L~ f2) ) by Def1;
take P1 = L~ f1; :: thesis:
take P2 = L~ f2; :: thesis:
thus P1 is_S-P_arc_joining p1,p2 by A2, A4, TOPREAL4:def 1; :: thesis:
thus P2 is_S-P_arc_joining p1,p2 by A3, A5, TOPREAL4:def 1; :: thesis:
thus ( P1 /\ P2 = {p1,p2} & P = P1 \/ P2 ) by A6; :: thesis: