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:8;
let x be set ; :: 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 m' being odd Element of NAT such that
A2: ( m' <= (2 * n) + 1 & [m',m] = x ) by Def3;
m' <= (2 * k) + 1 by A1, A2, XXREAL_0:2;
hence x in PFCrt k,m by A2, Def3; :: thesis: verum