theorem :: PARTIT_2:24

for S, X being non empty set
for R being Relation of X st R is antisymmetric holds
R is_antisymmetric_in S