let n, k be Element of NAT ; :: thesis: PFCrt n,k c= PFCrt (n + 1),k
PFCrt n,k c< PFCrt (n + 1),k by Th20;
hence PFCrt n,k c= PFCrt (n + 1),k by XBOOLE_0:def 8; :: thesis: verum