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