theorem :: ORDERS_1:74

for R being Relation
for X being set st R is_antisymmetric_in X holds
R |_2 X is antisymmetric by Lm10;