let P be Subset of (TOP-REAL 2); ( 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
; 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); ( 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
; 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; 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; ( 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; ( 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; ( P1 /\ P2 = {p1,p2} & P = P1 \/ P2 )
thus
( P1 /\ P2 = {p1,p2} & P = P1 \/ P2 )
by A9, A10; verum