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:1; :: thesis: verum