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 object ; :: 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