set n2 = n + 2;
A1: len (Permutations (n + 2)) = n + 2 by MATRIX_2:20;
n + 2 >= 2 + 0 by XREAL_1:8;
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;
not tr is even by A5, Th27;
hence not for b₁ being Permutation of (Seg (n + 2)) holds b₁ is even by A1; :: thesis: verum