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