let P be Subset of (TOP-REAL 2); :: thesis: ( P is special_polygonal implies not P is trivial )
assume P is special_polygonal ; :: thesis: not P is trivial
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 trivial by ZFMISC_1:def 10; :: thesis: verum