for X being set
for R being Relation holds
( R is_antisymmetric_in X iff R \ (id X) is_asymmetric_in X )