let n, n' be Element of NAT ; :: thesis: not PFCrt (n + 1),n' c= PFCrt n,n'
set k = [((2 * n) + 3),n'];
PFCrt (n + 1),n' = (PFCrt n,n') \/ {[((2 * n) + 3),n']} by Th19;
then {[((2 * n) + 3),n']} c= PFCrt (n + 1),n' by XBOOLE_1:7;
then A1: [((2 * n) + 3),n'] in PFCrt (n + 1),n' by ZFMISC_1:37;
PFCrt n,n' misses {[((2 * n) + 3),n']} by Th18;
then (PFCrt n,n') /\ {[((2 * n) + 3),n']} = {} by XBOOLE_0:def 7;
hence not PFCrt (n + 1),n' c= PFCrt n,n' by A1, ZFMISC_1:52; :: thesis: verum