:: deftheorem defines being_S-P_arc TOPREAL1:def 9 :
for P being Subset of (TOP-REAL 2) holds
( P is being_S-P_arc iff ex f being FinSequence of (TOP-REAL 2) st
( f is being_S-Seq & P = L~ f ) );