let V, V9, C, C9 be set ; :: thesis: ( V c= V9 & C c= C9 implies SubstitutionSet (V,C) c= SubstitutionSet (V9,C9) )
assume ( V c= V9 & C c= C9 ) ; :: thesis: SubstitutionSet (V,C) c= SubstitutionSet (V9,C9)
then A1: PFuncs (V,C) c= PFuncs (V9,C9) by PARTFUN1:50;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in SubstitutionSet (V,C) or x in SubstitutionSet (V9,C9) )
assume x in SubstitutionSet (V,C) ; :: thesis: x in SubstitutionSet (V9,C9)
then x in { A where A is Element of Fin (PFuncs (V,C)) : ( ( for u being set st u in A holds
u is finite ) & ( for s, t being Element of PFuncs (V,C) st s in A & t in A & s c= t holds
s = t ) ) } by SUBSTLAT:def 1;
then consider B being Element of Fin (PFuncs (V,C)) such that
A2: ( B = x & ( for u being set st u in B holds
u is finite ) ) and
A3: for s, t being Element of PFuncs (V,C) st s in B & t in B & s c= t holds
s = t ;
A4: ( B in Fin (PFuncs (V,C)) & Fin (PFuncs (V,C)) c= Fin (PFuncs (V9,C9)) ) by A1, FINSUB_1:10;
A5: B c= PFuncs (V,C) by FINSUB_1:def 5;
reconsider B = B as Element of Fin (PFuncs (V9,C9)) by A4;
for s, t being Element of PFuncs (V9,C9) st s in B & t in B & s c= t holds
s = t by A3, A5;
then x in { D where D is Element of Fin (PFuncs (V9,C9)) : ( ( for u being set st u in D holds
u is finite ) & ( for s, t being Element of PFuncs (V9,C9) st s in D & t in D & s c= t holds
s = t ) ) } by A2;
hence x in SubstitutionSet (V9,C9) by SUBSTLAT:def 1; :: thesis: verum