let X be set ; :: thesis: for fs being FinSequence of X holds fs is Subset of fs
let fs be FinSequence of X; :: thesis: fs is Subset of fs
fs c= fs ;
hence fs is Subset of fs ; :: thesis: verum