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