let R be Relation; :: thesis: for a, b being set st R is antisymmetric holds
( [a,b] in R \~ iff ( [a,b] in R & a <> b ) )
let a, b be set ; :: thesis: ( R is antisymmetric implies ( [a,b] in R \~ iff ( [a,b] in R & a <> b ) ) )
assume R is antisymmetric ; :: thesis: ( [a,b] in R \~ iff ( [a,b] in R & a <> b ) )
then A1: R is_antisymmetric_in field R by RELAT_2:def 12;
A2: R \~ is_asymmetric_in field (R \~) by RELAT_2:def 13;

hereby :: thesis: ( [a,b] in R & a <> b implies [a,b] in R \~ )

assume A3: [a,b] in R \~ ; :: thesis: ( [a,b] in R & a <> b )
hence [a,b] in R ; :: thesis: a <> b

now

assume A4: a = b ; :: thesis: contradiction
a in field (R \~) by A3, RELAT_1:30;
hence contradiction by A2, A3, A4, RELAT_2:def 5; :: thesis: verum

end;

hence a <> b ; :: thesis: verum

end;

assume that
A5: [a,b] in R and
A6: a <> b ; :: thesis: [a,b] in R \~
A7: a in field R by A5, RELAT_1:30;
b in field R by A5, RELAT_1:30;
then not [b,a] in R by A1, A5, A6, A7, RELAT_2:def 4;
then not [a,b] in R ~ by RELAT_1:def 7;
hence [a,b] in R \~ by A5, XBOOLE_0:def 5; :: thesis: verum