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