let X be set ; :: thesis: for Y being FinSequenceSet of X holds Y c= X *
let Y be FinSequenceSet of X; :: thesis: Y c= X *
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Y or x in X * )
assume x in Y ; :: thesis: x in X *
then x is FinSequence of X by FINSEQ_2:def 3;
hence x in X * by FINSEQ_1:def 11; :: thesis: verum