let P be Subset of (TOP-REAL 2); :: thesis: ( P is special_polygonal implies not P is empty )
assume P is special_polygonal ; :: thesis: not P is empty
then ex p1, p2 being Point of (TOP-REAL 2) st
( p1 <> p2 & p1 in P & p2 in P ) by Lm17;
hence not P is empty ; :: thesis: verum