reconsider f = id (Seg n) as Permutation of (Seg n) ;
f is even by MATRIX_2:29;
hence ex b₁ being Permutation of (Seg n) st b₁ is even ; :: thesis: verum