let k be Element of NAT ; :: thesis: for V, X being set
for a being Element of st X in a holds
X is finite Subset of
let V, X be set ; :: thesis: for a being Element of st X in a holds
X is finite Subset of
let a be Element of ; :: thesis: ( X in a implies X is finite Subset of )
assume A1: X in a ; :: thesis: X is finite Subset of
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 by A3, A1, A2, HEYTING2:2; :: thesis: verum