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
p1,p2 split P )
assume P is special_polygonal ; :: thesis: for p1, p2 being Point of (TOP-REAL 2) st p1 <> p2 & p1 in P & p2 in P holds
p1,p2 split P
then ex q1, q2 being Point of (TOP-REAL 2) st q1,q2 split P by Def2;
hence for p1, p2 being Point of (TOP-REAL 2) st p1 <> p2 & p1 in P & p2 in P holds
p1,p2 split P by Th57; :: thesis: verum