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 Th19;
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:37;
PFCrt (n,n9) misses {[((2 * n) + 3),n9]} by Th18;
then (PFCrt (n,n9)) /\ {[((2 * n) + 3),n9]} = {} by XBOOLE_0:def 7;
hence not PFCrt ((n + 1),n9) c= PFCrt (n,n9) by A1, ZFMISC_1:52; :: thesis: verum