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