thus ( P is being_special_polygon implies ex p1, p2 being Point of () st p1,p2 split P ) :: thesis: ( ex p1, p2 being Point of () st p1,p2 split P implies P is special_polygonal )
proof
given p1, p2 being Point of (), P1, P2 being Subset of () such that A1: p1 <> p2 and
p1 in P and
p2 in P and
A2: P1 is_S-P_arc_joining p1,p2 and
A3: P2 is_S-P_arc_joining p1,p2 and
A4: P1 /\ P2 = {p1,p2} and
A5: P = P1 \/ P2 ; :: according to TOPREAL4:def 2 :: thesis: ex p1, p2 being Point of () st p1,p2 split P
take p1 ; :: thesis: ex p2 being Point of () st p1,p2 split P
take p2 ; :: thesis: p1,p2 split P
thus p1 <> p2 by A1; :: according to SPPOL_2:def 1 :: thesis: ex f1, f2 being S-Sequence_in_R2 st
( p1 = f1 /. 1 & p1 = f2 /. 1 & p2 = f1 /. (len f1) & p2 = f2 /. (len f2) & (L~ f1) /\ (L~ f2) = {p1,p2} & P = (L~ f1) \/ (L~ f2) )

consider f1 being FinSequence of () such that
A6: f1 is being_S-Seq and
A7: P1 = L~ f1 and
A8: p1 = f1 /. 1 and
A9: p2 = f1 /. (len f1) by A2;
consider f2 being FinSequence of () such that
A10: f2 is being_S-Seq and
A11: P2 = L~ f2 and
A12: p1 = f2 /. 1 and
A13: p2 = f2 /. (len f2) by A3;
reconsider f1 = f1, f2 = f2 as S-Sequence_in_R2 by ;
take f1 ; :: thesis: ex f2 being S-Sequence_in_R2 st
( p1 = f1 /. 1 & p1 = f2 /. 1 & p2 = f1 /. (len f1) & p2 = f2 /. (len f2) & (L~ f1) /\ (L~ f2) = {p1,p2} & P = (L~ f1) \/ (L~ f2) )

take f2 ; :: thesis: ( p1 = f1 /. 1 & p1 = f2 /. 1 & p2 = f1 /. (len f1) & p2 = f2 /. (len f2) & (L~ f1) /\ (L~ f2) = {p1,p2} & P = (L~ f1) \/ (L~ f2) )
thus ( p1 = f1 /. 1 & p1 = f2 /. 1 & p2 = f1 /. (len f1) & p2 = f2 /. (len f2) & (L~ f1) /\ (L~ f2) = {p1,p2} & P = (L~ f1) \/ (L~ f2) ) by A4, A5, A7, A8, A9, A11, A12, A13; :: thesis: verum
end;
given p1, p2 being Point of () such that A14: p1,p2 split P ; :: thesis:
A15: p2 in {p1,p2} by TARSKI:def 2;
A16: p1 in {p1,p2} by TARSKI:def 2;
consider f1, f2 being S-Sequence_in_R2 such that
A17: p1 = f1 /. 1 and
A18: p1 = f2 /. 1 and
A19: p2 = f1 /. (len f1) and
A20: p2 = f2 /. (len f2) and
A21: (L~ f1) /\ (L~ f2) = {p1,p2} and
A22: P = (L~ f1) \/ (L~ f2) by A14;
take p1 ; :: according to TOPREAL4:def 2 :: thesis: ex b1 being Element of the carrier of () ex b2, b3 being Element of bool the carrier of () st
( not p1 = b1 & p1 in P & b1 in P & b2 is_S-P_arc_joining p1,b1 & b3 is_S-P_arc_joining p1,b1 & b2 /\ b3 = {p1,b1} & P = b2 \/ b3 )

take p2 ; :: thesis: ex b1, b2 being Element of bool the carrier of () st
( not p1 = p2 & p1 in P & p2 in P & b1 is_S-P_arc_joining p1,p2 & b2 is_S-P_arc_joining p1,p2 & b1 /\ b2 = {p1,p2} & P = b1 \/ b2 )

take P1 = L~ f1; :: thesis: ex b1 being Element of bool the carrier of () st
( not p1 = p2 & p1 in P & p2 in P & P1 is_S-P_arc_joining p1,p2 & b1 is_S-P_arc_joining p1,p2 & P1 /\ b1 = {p1,p2} & P = P1 \/ b1 )

take P2 = L~ f2; :: thesis: ( not p1 = p2 & p1 in P & p2 in P & 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 <> p2 by A14; :: thesis: ( p1 in P & p2 in P & 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} c= P by ;
hence ( p1 in P & p2 in P ) by ; :: 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 ex f being FinSequence of () st
( f is being_S-Seq & P1 = L~ f & p1 = f /. 1 & p2 = f /. (len f) ) by ; :: according to TOPREAL4:def 1 :: thesis: ( P2 is_S-P_arc_joining p1,p2 & P1 /\ P2 = {p1,p2} & P = P1 \/ P2 )
thus ex f being FinSequence of () st
( f is being_S-Seq & P2 = L~ f & p1 = f /. 1 & p2 = f /. (len f) ) by ; :: according to TOPREAL4:def 1 :: thesis: ( P1 /\ P2 = {p1,p2} & P = P1 \/ P2 )
thus ( P1 /\ P2 = {p1,p2} & P = P1 \/ P2 ) by ; :: thesis: verum