:: deftheorem defines is_asymmetric_in RELAT_2:def 5 :
for R being Relation
for X being set holds
( R is_asymmetric_in X iff for x, y being object st x in X & y in X & [x,y] in R holds
not [y,x] in R );