let X be non empty set ; :: thesis: for r being Relation of X st r is antisymmetric holds

chi (r,[:X,X:]) is antisymmetric

let r be Relation of X; :: thesis: ( r is antisymmetric implies chi (r,[:X,X:]) is antisymmetric )

assume r is antisymmetric ; :: thesis: chi (r,[:X,X:]) is antisymmetric

then A1: r is_antisymmetric_in field r by RELAT_2:def 12;

for x, y being Element of X st (chi (r,[:X,X:])) . (x,y) <> 0 & (chi (r,[:X,X:])) . (y,x) <> 0 holds

x = y

chi (r,[:X,X:]) is antisymmetric

let r be Relation of X; :: thesis: ( r is antisymmetric implies chi (r,[:X,X:]) is antisymmetric )

assume r is antisymmetric ; :: thesis: chi (r,[:X,X:]) is antisymmetric

then A1: r is_antisymmetric_in field r by RELAT_2:def 12;

for x, y being Element of X st (chi (r,[:X,X:])) . (x,y) <> 0 & (chi (r,[:X,X:])) . (y,x) <> 0 holds

x = y

proof

hence
chi (r,[:X,X:]) is antisymmetric
; :: thesis: verum
let x, y be Element of X; :: thesis: ( (chi (r,[:X,X:])) . (x,y) <> 0 & (chi (r,[:X,X:])) . (y,x) <> 0 implies x = y )

assume that

A2: (chi (r,[:X,X:])) . (x,y) <> 0 and

A3: (chi (r,[:X,X:])) . (y,x) <> 0 ; :: thesis: x = y

A4: ( x in field r & y in field r & [x,y] in r & [y,x] in r implies x = y ) by A1, RELAT_2:def 4;

[x,y] in r by A2, FUNCT_3:def 3;

hence x = y by A3, A4, FUNCT_3:def 3, RELAT_1:15; :: thesis: verum

end;assume that

A2: (chi (r,[:X,X:])) . (x,y) <> 0 and

A3: (chi (r,[:X,X:])) . (y,x) <> 0 ; :: thesis: x = y

A4: ( x in field r & y in field r & [x,y] in r & [y,x] in r implies x = y ) by A1, RELAT_2:def 4;

[x,y] in r by A2, FUNCT_3:def 3;

hence x = y by A3, A4, FUNCT_3:def 3, RELAT_1:15; :: thesis: verum