let P be Subset of (TOP-REAL 2); :: thesis: ( P is being_S-P_arc implies P is compact )

A1: I[01] is compact by HEINE:4, TOPMETR:20;

assume P is being_S-P_arc ; :: thesis: P is compact

then reconsider P = P as being_S-P_arc Subset of (TOP-REAL 2) ;

consider f being Function of I[01],((TOP-REAL 2) | P) such that

A2: f is being_homeomorphism by TOPREAL1:29;

A3: rng f = [#] ((TOP-REAL 2) | P) by A2, TOPS_2:def 5;

f is continuous by A2, TOPS_2:def 5;

then (TOP-REAL 2) | P is compact by A1, A3, COMPTS_1:14;

hence P is compact by COMPTS_1:3; :: thesis: verum

A1: I[01] is compact by HEINE:4, TOPMETR:20;

assume P is being_S-P_arc ; :: thesis: P is compact

then reconsider P = P as being_S-P_arc Subset of (TOP-REAL 2) ;

consider f being Function of I[01],((TOP-REAL 2) | P) such that

A2: f is being_homeomorphism by TOPREAL1:29;

A3: rng f = [#] ((TOP-REAL 2) | P) by A2, TOPS_2:def 5;

f is continuous by A2, TOPS_2:def 5;

then (TOP-REAL 2) | P is compact by A1, A3, COMPTS_1:14;

hence P is compact by COMPTS_1:3; :: thesis: verum