:: deftheorem Def2 defines antisymmetric MMLQUER2:def 2 :
for R being Relation holds
( R is antisymmetric iff for x, y being set st x,y in R & y,x in R holds
x = y );