let R be Relation; :: thesis: ( R is asymmetric implies ( R is irreflexive & R is antisymmetric ) )
assume A1: R is_asymmetric_in field R ; :: according to RELAT_2:def 13 :: thesis: ( R is irreflexive & R is antisymmetric )
then for x being set st x in field R holds
not [x,x] in R by Def5;
hence R is irreflexive by Def2, Def10; :: thesis: R is antisymmetric
for x, y being set st x in field R & y in field R & [x,y] in R & [y,x] in R holds
x = y by A1, Def5;
hence R is antisymmetric by Def4, Def12; :: thesis: verum