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: [((2 * n) + 1),m] in PFCrt n,m by Def3;
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 m' being odd Element of NAT st
( m' <= 2 * k & [m',m] = [((2 * n) + 1),m] ) or [(2 * k),m] = [((2 * n) + 1),m] ) by A4, Def2;

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

then consider m' being odd Element of NAT such that
A5: ( m' <= 2 * k & [m',m] = [((2 * n) + 1),m] ) ;
A6: (2 * n) + 1 <= 2 * k by A5, ZFMISC_1:33;
2 * k <= 2 * n by A2, NAT_1:4;
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;

hence contradiction by A1, A3; :: thesis: verum

end;

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