[(2 * n),k] in PFArt (n,k) by Def2;
hence not PFArt (n,k) is empty ; :: thesis: verum