let n, k be Element of NAT ; :: thesis: 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]} :: according to XBOOLE_0:def 10 :: thesis: (PFCrt n,k) \/ {[((2 * n) + 3),k]} c= PFCrt (n + 1),k

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in PFCrt (n + 1),k or x in (PFCrt n,k) \/ {[((2 * n) + 3),k]} )
assume x in PFCrt (n + 1),k ; :: thesis: x in (PFCrt n,k) \/ {[((2 * n) + 3),k]}
then consider m being odd Element of NAT such that
A2: m <= (2 * (n + 1)) + 1 and
A3: [m,k] = x by Def3;

per cases ( m <= 2 * (n + 1) or m = (2 * (n + 1)) + 1 ) by A2, NAT_1:9;

suppose m <= 2 * (n + 1) ; :: thesis: x in (PFCrt n,k) \/ {[((2 * n) + 3),k]}

then ( m <= (2 * n) + 1 or m = ((2 * n) + 1) + 1 ) by NAT_1:8;
then x in PFCrt n,k by A3, Def3;
hence x in (PFCrt n,k) \/ {[((2 * n) + 3),k]} by XBOOLE_0:def 3; :: thesis: verum

end;

suppose m = (2 * (n + 1)) + 1 ; :: thesis: x in (PFCrt n,k) \/ {[((2 * n) + 3),k]}

then x in {[((2 * n) + 3),k]} by A3, TARSKI:def 1;
hence x in (PFCrt n,k) \/ {[((2 * n) + 3),k]} by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( 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]} ; :: thesis: x in PFCrt (n + 1),k

per cases ( x in PFCrt n,k or x in {[((2 * n) + 3),k]} ) by A4, XBOOLE_0:def 3;

suppose x in PFCrt n,k ; :: thesis: x in PFCrt (n + 1),k

then consider m being odd Element of NAT such that
A5: m <= (2 * n) + 1 and
A6: [m,k] = x by Def3;
(2 * n) + 1 <= (2 * (n + 1)) + 1 by Lm4;
then m <= (2 * (n + 1)) + 1 by A5, XXREAL_0:2;
hence x in PFCrt (n + 1),k by A6, Def3; :: thesis: verum

end;

suppose x in {[((2 * n) + 3),k]} ; :: thesis: x in PFCrt (n + 1),k

then x = [((2 * n) + 3),k] by TARSKI:def 1;
hence x in PFCrt (n + 1),k by A1, Def3; :: thesis: verum

end;

end;