theorem :: PARTIT_2:28

for S, X being non empty set
for R being Relation of X st R is asymmetric holds
R is_asymmetric_in S