let D be set ; :: thesis: for D9 being FinSequenceSet of D holds D9 c= D *
let D9 be FinSequenceSet of D; :: thesis: D9 c= D *
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in D9 or a in D * )
assume a in D9 ; :: thesis: a in D *
then a is FinSequence of D by Def3;
hence a in D * by FINSEQ_1:def 11; :: thesis: verum