theorem :: RELAT_2:22

for R being Relation holds
( R is antisymmetric iff R /\ (R ~) c= id (dom R) )