lines M is Subset of ;
hence M is FinSequence of by FINSEQ_1:def 4; :: thesis: verum