let R be Relation; for X being set st R is_antisymmetric_in X holds
R ~ is_antisymmetric_in X
let X be set ; ( R is_antisymmetric_in X implies R ~ is_antisymmetric_in X )
assume A1:
for x, y being object st x in X & y in X & [x,y] in R & [y,x] in R holds
x = y
; RELAT_2:def 4 R ~ is_antisymmetric_in X
let x, y be object ; RELAT_2:def 4 ( not x in X or not y in X or not [x,y] in R ~ or not [y,x] in R ~ or x = y )
assume that
A2:
x in X
and
A3:
y in X
and
A4:
[x,y] in R ~
and
A5:
[y,x] in R ~
; x = y
A6:
[y,x] in R
by A4, RELAT_1:def 7;
[x,y] in R
by A5, RELAT_1:def 7;
hence
x = y
by A1, A2, A3, A6; verum