let R be Relation; :: thesis: ( R is asymmetric implies ( R is irreflexive & R is antisymmetric ) )
assume R is asymmetric ; :: thesis: ( R is irreflexive & R is antisymmetric )
then A1: R is_asymmetric_in field R by Def13;
then for x being set st x in field R holds
not [x,x] in R by Def5;
then R is_irreflexive_in field R by Def2;
hence R is irreflexive by 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;
then R is_antisymmetric_in field R by Def4;
hence R is antisymmetric by Def12; :: thesis: verum