let n, m, k be Element of NAT ; :: thesis: ( n <= k implies PFCrt (n,m) c= PFCrt (k,m) )
assume n <= k ; :: thesis: 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 ; :: according to TARSKI:def 3 :: thesis: ( not x in PFCrt (n,m) or x in PFCrt (k,m) )
assume x in PFCrt (n,m) ; :: thesis: 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; :: thesis: verum