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 and
p in G and
q in G and
A1: P1 is_S-P_arc_joining p,q and
A2: P2 is_S-P_arc_joining p,q and
P1 /\ P2 = {p,q} and
A3: G = P1 \/ P2 by TOPREAL4:def 2;
reconsider P1 = P1, P2 = P2 as Subset of (TOP-REAL 2) ;
A4: P2 is compact by A2, Th57, TOPREAL4:1;
P1 is compact by A1, Th57, TOPREAL4:1;
hence G is compact by A3, A4, COMPTS_1:10; :: thesis: verum