let n, n9 be Element of NAT ; not PFCrt ((n + 1),n9) c= PFCrt (n,n9)
set k = [((2 * n) + 3),n9];
PFCrt ((n + 1),n9) = (PFCrt (n,n9)) \/ {[((2 * n) + 3),n9]}
by Th16;
then
{[((2 * n) + 3),n9]} c= PFCrt ((n + 1),n9)
by XBOOLE_1:7;
then A1:
[((2 * n) + 3),n9] in PFCrt ((n + 1),n9)
by ZFMISC_1:31;
PFCrt (n,n9) misses {[((2 * n) + 3),n9]}
by Th15;
then
(PFCrt (n,n9)) /\ {[((2 * n) + 3),n9]} = {}
;
hence
not PFCrt ((n + 1),n9) c= PFCrt (n,n9)
by A1, ZFMISC_1:46; verum