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}:] )
A1: SubstitutionSet V,{k} = the carrier of (SubstPoset V,{k}) by SUBSTLAT:def 4;
then a in SubstitutionSet V,{k} ;
then A2: ( a c= PFuncs V,{k} & a is finite ) by FINSUB_1:def 5;
assume A3: X in a ; :: thesis: X is finite Subset of [:V,{k}:]
then A4: X in PFuncs V,{k} by A2;
PFuncs V,{k} c= bool [:V,{k}:] by HEYTING2:4;
hence X is finite Subset of [:V,{k}:] by A1, A3, A4, HEYTING2:2; :: thesis: verum