let D1, D2 be set ; :: thesis: ( D1 c= D2 implies D1 ** c= D2 ** )
assume A1: D1 c= D2 ; :: thesis: D1 ** c= D2 **
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in D1 ** or x in D2 ** )
assume x in D1 ** ; :: thesis: x in D2 **
then reconsider p = x as one-to-one FinSequence of D1 by Def2;
rng p c= D2 by A1;
then x is one-to-one FinSequence of D2 by FINSEQ_1:def 4;
hence x in D2 ** by Def2; :: thesis: verum