let n, i, j be Nat; :: thesis:
assume that
A1: i in Seg n and
A2: j in Seg n and
A3: i < j ; :: thesis:
set P = Permutations n;
consider tr being Element of Permutations n such that
A4: tr is being_transposition and
A5: tr . i = j by A1, A2, A3, Th16;
{i,j} in 2Set (Seg n) by A1, A2, A3, Th1;
then reconsider n2 = n - 2 as Nat by Th2, NAT_1:21, NAT_1:23;
set ODD = { q where q is Element of Permutations n : q is odd } ;
set EVEN = { p where p is Element of Permutations n : p is even } ;
A6: { p where p is Element of Permutations n : p is even } c= Permutations n

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in { p where p is Element of Permutations n : p is even } ; :: thesis:
then ex p being Element of Permutations n st
( p = x & p is even ) ;
hence x in Permutations n ; :: thesis:

end;

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in { q where q is Element of Permutations n : q is odd } ; :: thesis:
then ex q being Element of Permutations n st
( q = x & q is odd ) ;
hence x in Permutations n ; :: thesis:

end;

then reconsider O = { q where q is Element of Permutations n : q is odd } , E = { p where p is Element of Permutations n : p is even } as finite set by A6;
take O ; :: thesis:
take E ; :: thesis:
thus ( E = { p where p is Element of Permutations n : p is even } & O = { q where q is Element of Permutations n : q is odd } ) ; :: thesis:
thus E /\ O = {} :: thesis:

end;

end;