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