theorem :: JORDAN5B:31

for f being constant standard special_circular_sequence
for j being Nat
for P being Subset of (TOP-REAL 2) st 1 <= j & j <= width (GoB f) & P = LSeg (((GoB f) * (1,j)),((GoB f) * ((len (GoB f)),j))) holds
P is_S-P_arc_joining (GoB f) * (1,j),(GoB f) * ((len (GoB f)),j)