let n, m, k be Element of NAT ; :: thesis: ( PFCrt n,m c= PFArt k,m iff n < k )
thus ( PFCrt n,m c= PFArt k,m implies n < k ) :: thesis: ( n < k implies PFCrt n,m c= PFArt k,m )

proof

assume A1: PFCrt n,m c= PFArt k,m ; :: thesis: n < k
assume A2: k <= n ; :: thesis: contradiction
A3: not [((2 * n) + 1),m] in PFArt k,m

proof

assume A4: [((2 * n) + 1),m] in PFArt k,m ; :: thesis: contradiction

per cases ( ex m9 being odd Element of NAT st
( m9 <= 2 * k & [m9,m] = [((2 * n) + 1),m] ) or [(2 * k),m] = [((2 * n) + 1),m] ) by A4, Def2;

suppose A5: ex m9 being odd Element of NAT st
( m9 <= 2 * k & [m9,m] = [((2 * n) + 1),m] ) ; :: thesis: contradiction

A6: 2 * k <= 2 * n by A2, NAT_1:4;
(2 * n) + 1 <= 2 * k by A5, ZFMISC_1:33;
hence contradiction by A6, NAT_1:13; :: thesis: verum

end;

suppose [(2 * k),m] = [((2 * n) + 1),m] ; :: thesis: contradiction

hence contradiction by ZFMISC_1:33; :: thesis: verum

end;

end;

end;

[((2 * n) + 1),m] in PFCrt n,m by Def3;
hence contradiction by A1, A3; :: thesis: verum

end;

thus ( n < k implies PFCrt n,m c= PFArt k,m ) by Lm7; :: thesis: verum