let P be Subset of (TOP-REAL 2); :: thesis: ( P is special_polygonal implies for p1, p2 being Point of (TOP-REAL 2) st p1 <> p2 & p1 in P & p2 in P holds

ex P1, P2 being Subset of (TOP-REAL 2) 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 (TOP-REAL 2) st p1 <> p2 & p1 in P & p2 in P holds

ex P1, P2 being Subset of (TOP-REAL 2) 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 (TOP-REAL 2); :: thesis: ( p1 <> p2 & p1 in P & p2 in P implies ex P1, P2 being Subset of (TOP-REAL 2) 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 (TOP-REAL 2) 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 (TOP-REAL 2) 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 A9, A10; :: thesis: verum

ex P1, P2 being Subset of (TOP-REAL 2) 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 (TOP-REAL 2) st p1 <> p2 & p1 in P & p2 in P holds

ex P1, P2 being Subset of (TOP-REAL 2) 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 (TOP-REAL 2); :: thesis: ( p1 <> p2 & p1 in P & p2 in P implies ex P1, P2 being Subset of (TOP-REAL 2) 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 (TOP-REAL 2) 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 (TOP-REAL 2) 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 A9, A10; :: thesis: verum