theorem :: GLIBPRE1:10

for X being set
for R being Relation of X holds
( R is antisymmetric iff R \ (id X) is asymmetric )