let n, k be Element of NAT ; :: thesis: {(PFArt (n,k))} is Element of (SubstPoset (NAT,{k}))
SubstitutionSet (NAT,{k}) = the carrier of (SubstPoset (NAT,{k})) by SUBSTLAT:def 4;
hence {(PFArt (n,k))} is Element of (SubstPoset (NAT,{k})) by HEYTING2:2; :: thesis: verum