for p being FinSubsequence holds rng (Seq p) c= rng p by RELAT_1:26;