let n, m, k be Element of NAT ; :: thesis: not PFArt n,m c= PFCrt k,m
set x = [(2 * n),m];
A1: not [(2 * n),m] in PFCrt k,m

proof

assume [(2 * n),m] in PFCrt k,m ; :: thesis: contradiction
then ex m9 being odd Element of NAT st
( m9 <= (2 * k) + 1 & [m9,m] = [(2 * n),m] ) by Def3;
hence contradiction by ZFMISC_1:33; :: thesis: verum

end;

[(2 * n),m] in PFArt n,m by Def2;
hence not PFArt n,m c= PFCrt k,m by A1; :: thesis: verum