let n, m, k be Element of NAT ; :: thesis: ( PFArt (n,m) c= PFArt (k,m) implies n = k )
assume A1: PFArt (n,m) c= PFArt (k,m) ; :: thesis: n = k
assume n <> k ; :: thesis: contradiction
then 2 * n <> 2 * k ;
then A2: [(2 * n),m] <> [(2 * k),m] by XTUPLE_0:1;
[(2 * n),m] in PFArt (n,m) by Def2;
then ex m9 being odd Element of NAT st
( m9 <= 2 * k & [m9,m] = [(2 * n),m] ) by A1, A2, Def2;
hence contradiction by XTUPLE_0:1; :: thesis: verum