let n, k be Element of NAT ; PFCrt (n,k) misses {[((2 * n) + 3),k]}
assume
(PFCrt (n,k)) /\ {[((2 * n) + 3),k]} <> {}
; XBOOLE_0:def 7 contradiction
then consider x being object such that
A1:
x in (PFCrt (n,k)) /\ {[((2 * n) + 3),k]}
by XBOOLE_0:def 1;
x in PFCrt (n,k)
by A1, XBOOLE_0:def 4;
then consider m being odd Element of NAT such that
A2:
m <= (2 * n) + 1
and
A3:
[m,k] = x
by Def3;
x in {[((2 * n) + 3),k]}
by A1, XBOOLE_0:def 4;
then
x = [((2 * n) + 3),k]
by TARSKI:def 1;
then
m = (2 * n) + 3
by A3, XTUPLE_0:1;
hence
contradiction
by A2, XREAL_1:6; verum