let s1 be subsequence of s; :: thesis: s1 is non-empty
rng s1 c= rng s by Th21;
hence not {} in rng s1 ; :: according to RELAT_1:def 9 :: thesis: verum