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

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