set n2 = n + 2;
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
A1: ( i in Seg (n + 2) & j in Seg (n + 2) & i < j & {1,2} = {i,j} ) by Th1;
consider tr being Element of Permutations (n + 2) such that
A2: ( tr is being_transposition & tr . i = j ) by A1, Th16;
( not tr is even & len (Permutations (n + 2)) = n + 2 ) by A2, Th27, MATRIX_2:20;
hence not for b₁ being Permutation of (Seg (n + 2)) holds b₁ is even ; :: thesis: verum