let S be SubSpace of TOP-REAL 2; :: thesis: ( S is being_simple_closed_curve implies ( not S is empty & S is pathwise_connected & S is compact ) )

assume A1: the carrier of S is Simple_closed_curve ; :: according to TOPREALB:def 5 :: thesis: ( not S is empty & S is pathwise_connected & S is compact )

then reconsider A = the carrier of S as Simple_closed_curve ;

not A is empty ;

hence not the carrier of S is empty ; :: according to STRUCT_0:def 1 :: thesis: ( S is pathwise_connected & S is compact )

thus S is pathwise_connected by A1, TOPALG_3:10; :: thesis: S is compact

[#] S = A ;

then [#] S is compact by COMPTS_1:2;

hence S is compact by COMPTS_1:1; :: thesis: verum

assume A1: the carrier of S is Simple_closed_curve ; :: according to TOPREALB:def 5 :: thesis: ( not S is empty & S is pathwise_connected & S is compact )

then reconsider A = the carrier of S as Simple_closed_curve ;

not A is empty ;

hence not the carrier of S is empty ; :: according to STRUCT_0:def 1 :: thesis: ( S is pathwise_connected & S is compact )

thus S is pathwise_connected by A1, TOPALG_3:10; :: thesis: S is compact

[#] S = A ;

then [#] S is compact by COMPTS_1:2;

hence S is compact by COMPTS_1:1; :: thesis: verum