:: deftheorem defines antisymmetric YELLOW_0:def 3 :
for A being RelStr holds
( A is antisymmetric iff for x, y being Element of A st x <= y & y <= x holds
x = y );