theorem :: PARTIT_2:25

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