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