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

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