let P, Q be FinSequence-membered set ; :: thesis: ( Q c= P * implies Q * c= P * )
assume A1: Q c= P * ; :: thesis: Q * c= P *
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in Q * or a in P * )
assume a in Q * ; :: thesis: a in P *
then consider n being Nat such that
A2: a in Q ^^ n by Th5;
Q ^^ n c= P * by Th14, A1;
hence a in P * by A2; :: thesis: verum