let R be Relation; :: thesis: ( R is asymmetric implies ( R is irreflexive & R is antisymmetric ) )

assume A5: R is_asymmetric_in field R ; :: according to RELAT_2:def 13 :: thesis: ( R is irreflexive & R is antisymmetric )

then for x being object st x in field R holds

not [x,x] in R ;

hence R is irreflexive by Def2; :: thesis: R is antisymmetric

for x, y being object st x in field R & y in field R & [x,y] in R & [y,x] in R holds

x = y by A5;

hence R is antisymmetric by Def4; :: thesis: verum

assume A5: R is_asymmetric_in field R ; :: according to RELAT_2:def 13 :: thesis: ( R is irreflexive & R is antisymmetric )

then for x being object st x in field R holds

not [x,x] in R ;

hence R is irreflexive by Def2; :: thesis: R is antisymmetric

for x, y being object st x in field R & y in field R & [x,y] in R & [y,x] in R holds

x = y by A5;

hence R is antisymmetric by Def4; :: thesis: verum