let k be Element of NAT ; :: thesis: for V, X being set
for a being Element of (SubstPoset V,{k}) st X in a holds
X is finite Subset of [:V,{k}:]
let V, X be set ; :: thesis: for a being Element of (SubstPoset V,{k}) st X in a holds
X is finite Subset of [:V,{k}:]
let a be Element of (SubstPoset V,{k}); :: thesis: ( X in a implies X is finite Subset of [:V,{k}:] )
assume A1: X in a ; :: thesis: X is finite Subset of [:V,{k}:]
A2: PFuncs V,{k} c= bool [:V,{k}:] by PRE_POLY:16;
A3: SubstitutionSet V,{k} = the carrier of (SubstPoset V,{k}) by SUBSTLAT:def 4;
then a in SubstitutionSet V,{k} ;
then a c= PFuncs V,{k} by FINSUB_1:def 5;
then X in PFuncs V,{k} by A1;
hence X is finite Subset of [:V,{k}:] by A3, A1, A2, HEYTING2:2; :: thesis: verum