let P1 be Subset of (TOP-REAL 2); :: thesis: ( P1 is being_S-P_arc implies P1 <> {} )
assume P1 is being_S-P_arc ; :: thesis: P1 <> {}
then consider f being FinSequence of (TOP-REAL 2) such that
A1: f is being_S-Seq and
A2: P1 = L~ f ;
len f >= 2 by A1;
hence P1 <> {} by A2, Th23; :: thesis: verum