theorem :: SPRECT_3:39

for f being rectangular special_circular_sequence
for g being S-Sequence_in_R2 st g /. 1 in LeftComp f & g /. (len g) in RightComp f holds
Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)) <> SE-corner (L~ f)