let n, m, k be Element of NAT ; ( n <= k implies PFCrt (n,m) c= PFCrt (k,m) )
assume
n <= k
; PFCrt (n,m) c= PFCrt (k,m)
then
2 * n <= 2 * k
by NAT_1:4;
then A1:
(2 * n) + 1 <= (2 * k) + 1
by XREAL_1:6;
let x be object ; TARSKI:def 3 ( not x in PFCrt (n,m) or x in PFCrt (k,m) )
assume
x in PFCrt (n,m)
; x in PFCrt (k,m)
then consider m9 being odd Element of NAT such that
A2:
m9 <= (2 * n) + 1
and
A3:
[m9,m] = x
by Def3;
m9 <= (2 * k) + 1
by A1, A2, XXREAL_0:2;
hence
x in PFCrt (k,m)
by A3, Def3; verum