let n, n9 be Element of NAT ; :: thesis: 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; :: thesis: verum