theorem :: DICKSON:14

for R being Relation
for a, b being set st R is antisymmetric holds
( [a,b] in R \~ iff ( [a,b] in R & a <> b ) )