let n, k be Element of NAT ; PFCrt ((n + 1),k) = (PFCrt (n,k)) \/ {[((2 * n) + 3),k]}
A1:
(2 * (n + 1)) + 1 = (2 * n) + 3
;
thus
PFCrt ((n + 1),k) c= (PFCrt (n,k)) \/ {[((2 * n) + 3),k]}
XBOOLE_0:def 10 (PFCrt (n,k)) \/ {[((2 * n) + 3),k]} c= PFCrt ((n + 1),k)
let x be object ; TARSKI:def 3 ( not x in (PFCrt (n,k)) \/ {[((2 * n) + 3),k]} or x in PFCrt ((n + 1),k) )
assume A4:
x in (PFCrt (n,k)) \/ {[((2 * n) + 3),k]}
; x in PFCrt ((n + 1),k)