let G be Special_polygon_in_R2; 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; verum