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 A1: R is antisymmetric ; :: thesis: ( [a,b] in R \~ iff ( [a,b] in R & a <> b ) )
A2: R is_antisymmetric_in field R by A1, RELAT_2:def 12;
A3: 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 A4: [a,b] in R \~ ; :: thesis: ( [a,b] in R & a <> b )
hence [a,b] in R ; :: thesis: a <> b

now

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

end;

hence a <> b ; :: thesis: verum

end;

assume A6: ( [a,b] in R & a <> b ) ; :: thesis: [a,b] in R \~
then ( a in field R & b in field R ) by RELAT_1:30;
then not [b,a] in R by A2, A6, RELAT_2:def 4;
then not [a,b] in R ~ by RELAT_1:def 7;
hence [a,b] in R \~ by A6, XBOOLE_0:def 5; :: thesis: verum