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

proof

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 ( (chi r,[:X,X:]) . x,y <> 0 & (chi r,[:X,X:]) . y,x <> 0 ) ; :: thesis: x = y
then A2: ( [x,y] in r & [y,x] in r ) by FUNCT_3:def 3;
( 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;
hence x = y by A2, RELAT_1:30; :: thesis: verum

end;

hence chi r,[:X,X:] is antisymmetric by Def8; :: thesis: verum