let t be object ; :: 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 ABIAN:12;
then m in Seg ((2 * n) + 1) by A1, FINSEQ_1:1;
hence t in [:(Seg ((2 * n) + 1)),{k}:] by A2, ZFMISC_1:106; :: thesis: verum