let P be Subset of (TOP-REAL 2); :: thesis: ( P is special_polygonal implies ex p1, p2 being Point of (TOP-REAL 2) st
( p1 <> p2 & p1 in P & p2 in P ) )
assume P is special_polygonal ; :: thesis: ex p1, p2 being Point of (TOP-REAL 2) st
( p1 <> p2 & p1 in P & p2 in P )
then ex p1, p2 being Point of (TOP-REAL 2) ex P1, P2 being Subset of (TOP-REAL 2) st
( 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 ) by TOPREAL4:def 2;
hence ex p1, p2 being Point of (TOP-REAL 2) st
( p1 <> p2 & p1 in P & p2 in P ) ; :: thesis: verum