set x = PFCrt n,k;
PFCrt n,k c= [:(Seg ((2 * n) + 1)),{k}:]

proof

let t be set ; :: according to TARSKI:def 3 :: thesis: ( not t in PFCrt n,k or t in [:(Seg ((2 * n) + 1)),{k}:] )
assume t in PFCrt n,k ; :: thesis: t in [:(Seg ((2 * n) + 1)),{k}:]
then consider m being odd Element of NAT such that
A1: m <= (2 * n) + 1 and
A2: [m,k] = t by Def3;
1 <= m by Th1;
then m in Seg ((2 * n) + 1) by A1, FINSEQ_1:3;
hence t in [:(Seg ((2 * n) + 1)),{k}:] by A2, ZFMISC_1:129; :: thesis: verum

end;

hence PFCrt n,k is finite ; :: thesis: verum