let G be Special_polygon_in_R2; :: thesis: G is compact
consider p, q being Point of (TOP-REAL 2), P1, P2 being Subset of (TOP-REAL 2) such that
( p <> q & p in G & q in G ) and
A1: ( P1 is_S-P_arc_joining p,q & P2 is_S-P_arc_joining p,q ) and
P1 /\ P2 = {p,q} and
A2: G = P1 \/ P2 by TOPREAL4:def 2;
reconsider P1 = P1, P2 = P2 as Subset of (TOP-REAL 2) ;
( P1 is compact & P2 is compact ) by A1, Th62, TOPREAL4:2;
hence G is compact by A2, COMPTS_1:19; :: thesis: verum