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 & P1 = L~ f ) by Def11;
len f >= 2 by A1, Def10;
hence P1 <> {} by A1, Th29; :: thesis: verum