:: deftheorem Def13 defines asymmetric RELAT_2:def 13 :
for R being Relation holds
( R is asymmetric iff R is_asymmetric_in field R );