theorem :: ORDERS_1:81

for R being Relation
for X being set st R is_antisymmetric_in X holds
R ~ is_antisymmetric_in X by Lm14;