let X be non empty set ; for r being Relation of X st r is antisymmetric holds
chi (r,[:X,X:]) is antisymmetric
let r be Relation of X; ( r is antisymmetric implies chi (r,[:X,X:]) is antisymmetric )
assume
r is antisymmetric
; 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;
( (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
;
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;
verum
end;
hence
chi (r,[:X,X:]) is antisymmetric
; verum