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 object ; :: 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 object ; :: 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;