theorem LemAntisym: :: PREFER_1:31

for X being object
for R being Relation holds
( R is antisymmetric iff for x, y being object st [x,y] in R & [y,x] in R holds
x = y )