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 Th17;
hence PFCrt (n,k) c= PFCrt ((n + 1),k) ; :: thesis: verum