thus
( P is being_special_polygon implies ex p1, p2 being Point of (TOP-REAL 2) st p1,p2 split P )
:: thesis: ( ex p1, p2 being Point of (TOP-REAL 2) st p1,p2 split P implies P is special_polygonal )

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 b_{1} being Element of the carrier of (TOP-REAL 2) ex b_{2}, b_{3} being Element of bool the carrier of (TOP-REAL 2) st

( not p1 = b_{1} & p1 in P & b_{1} in P & b_{2} is_S-P_arc_joining p1,b_{1} & b_{3} is_S-P_arc_joining p1,b_{1} & b_{2} /\ b_{3} = {p1,b_{1}} & P = b_{2} \/ b_{3} )

take p2 ; :: thesis: ex b_{1}, b_{2} being Element of bool the carrier of (TOP-REAL 2) st

( not p1 = p2 & p1 in P & p2 in P & b_{1} is_S-P_arc_joining p1,p2 & b_{2} is_S-P_arc_joining p1,p2 & b_{1} /\ b_{2} = {p1,p2} & P = b_{1} \/ b_{2} )

take P1 = L~ f1; :: thesis: ex b_{1} being Element of bool the carrier of (TOP-REAL 2) st

( not p1 = p2 & p1 in P & p2 in P & P1 is_S-P_arc_joining p1,p2 & b_{1} is_S-P_arc_joining p1,p2 & P1 /\ b_{1} = {p1,p2} & P = P1 \/ b_{1} )

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 A21, A22, XBOOLE_1:29;

hence ( p1 in P & p2 in P ) by A16, A15; :: 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 (TOP-REAL 2) st

( f is being_S-Seq & P1 = L~ f & p1 = f /. 1 & p2 = f /. (len f) ) by A17, A19; :: 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 (TOP-REAL 2) st

( f is being_S-Seq & P2 = L~ f & p1 = f /. 1 & p2 = f /. (len f) ) by A18, A20; :: according to TOPREAL4:def 1 :: thesis: ( P1 /\ P2 = {p1,p2} & P = P1 \/ P2 )

thus ( P1 /\ P2 = {p1,p2} & P = P1 \/ P2 ) by A21, A22; :: thesis: verum

proof

given p1, p2 being Point of (TOP-REAL 2) such that A14:
p1,p2 split P
; :: thesis: P is special_polygonal
given p1, p2 being Point of (TOP-REAL 2), P1, P2 being Subset of (TOP-REAL 2) 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 (TOP-REAL 2) st p1,p2 split P

take p1 ; :: thesis: ex p2 being Point of (TOP-REAL 2) 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 (TOP-REAL 2) 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 (TOP-REAL 2) 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 A6, A10;

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;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 (TOP-REAL 2) st p1,p2 split P

take p1 ; :: thesis: ex p2 being Point of (TOP-REAL 2) 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 (TOP-REAL 2) 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 (TOP-REAL 2) 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 A6, A10;

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

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 b

( not p1 = b

take p2 ; :: thesis: ex b

( not p1 = p2 & p1 in P & p2 in P & b

take P1 = L~ f1; :: thesis: ex b

( not p1 = p2 & p1 in P & p2 in P & P1 is_S-P_arc_joining p1,p2 & b

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 A21, A22, XBOOLE_1:29;

hence ( p1 in P & p2 in P ) by A16, A15; :: 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 (TOP-REAL 2) st

( f is being_S-Seq & P1 = L~ f & p1 = f /. 1 & p2 = f /. (len f) ) by A17, A19; :: 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 (TOP-REAL 2) st

( f is being_S-Seq & P2 = L~ f & p1 = f /. 1 & p2 = f /. (len f) ) by A18, A20; :: according to TOPREAL4:def 1 :: thesis: ( P1 /\ P2 = {p1,p2} & P = P1 \/ P2 )

thus ( P1 /\ P2 = {p1,p2} & P = P1 \/ P2 ) by A21, A22; :: thesis: verum