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 XTUPLE_0:1; :: 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