let n, k be Element of NAT ; :: thesis: PFCrt n,k c< PFCrt (n + 1),k
thus PFCrt n,k c= PFCrt (n + 1),k :: according to XBOOLE_0:def 8 :: thesis: not PFCrt n,k = PFCrt (n + 1),k

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in PFCrt n,k or x in PFCrt (n + 1),k )
assume x in PFCrt n,k ; :: thesis: x in PFCrt (n + 1),k
then consider m being odd Element of NAT such that
A1: m <= (2 * n) + 1 and
A2: [m,k] = x by Def3;
(2 * n) + 1 <= (2 * (n + 1)) + 1 by Lm4;
then m <= (2 * (n + 1)) + 1 by A1, XXREAL_0:2;
hence x in PFCrt (n + 1),k by A2, Def3; :: thesis: verum

end;

thus not PFCrt n,k = PFCrt (n + 1),k by Lm5; :: thesis: verum