set n2 = n + 2;
A1: len (Permutations (n + 2)) = n + 2 by MATRIX_1:9;
n + 2 >= 2 + 0 by XREAL_1:6;
then {1,2} in 2Set (Seg (n + 2)) by Th3;
then consider i, j being Nat such that
A2: i in Seg (n + 2) and
A3: j in Seg (n + 2) and
A4: i < j and
{1,2} = {i,j} by Th1;
consider tr being Element of Permutations (n + 2) such that
A5: tr is being_transposition and
tr . i = j by A2, A3, A4, Th16;
tr is odd by A5, Th27;
hence ex b₁ being Permutation of (Seg (n + 2)) st b₁ is odd by A1; :: thesis: verum