let x, y, z be set ; for O being non empty connected Poset
for R being array of O st [x,y] in inversions R holds
( ( [z,y] in inversions R & z in x ) iff [z,x] in inversions (Swap (R,x,y)) )
let O be non empty connected Poset; for R being array of O st [x,y] in inversions R holds
( ( [z,y] in inversions R & z in x ) iff [z,x] in inversions (Swap (R,x,y)) )
let R be array of O; ( [x,y] in inversions R implies ( ( [z,y] in inversions R & z in x ) iff [z,x] in inversions (Swap (R,x,y)) ) )
set s = Swap (R,x,y);
assume
[x,y] in inversions R
; ( ( [z,y] in inversions R & z in x ) iff [z,x] in inversions (Swap (R,x,y)) )
then A1:
( x in dom R & y in dom R & x in y & R /. x > R /. y )
by Th46;
then A2:
( (Swap (R,x,y)) /. x = R /. y & (Swap (R,x,y)) /. y = R /. x & dom (Swap (R,x,y)) = dom R )
by Th30, Th32, FUNCT_7:99;
hereby ( [z,x] in inversions (Swap (R,x,y)) implies ( [z,y] in inversions R & z in x ) )
assume A3:
(
[z,y] in inversions R &
z in x )
;
[z,x] in inversions (Swap (R,x,y))then A4:
(
z in dom R &
z in y &
R /. z > R /. y )
by Th46;
then
(
x <> z &
y <> z )
by A3;
then
(Swap (R,x,y)) /. z = R /. z
by A4, Th34;
hence
[z,x] in inversions (Swap (R,x,y))
by A3, A1, A2, A4;
verum
end;
assume
[z,x] in inversions (Swap (R,x,y))
; ( [z,y] in inversions R & z in x )
then A5:
( z in dom R & z in x & (Swap (R,x,y)) /. z > (Swap (R,x,y)) /. x )
by A2, Th46;
then A6:
z in y
by A1, ORDINAL1:10;
(Swap (R,x,y)) /. z = R /. z
by A1, A5, Th34;
hence
( [z,y] in inversions R & z in x )
by A1, A2, A5, A6; verum