let R be Relation; :: thesis: ( R is irreflexive & R is transitive implies R is asymmetric )
assume that
A1: R is irreflexive and
A2: R is transitive ; :: thesis: R is asymmetric
A3: R is_irreflexive_in field R by A1, Def10;
A4: R is_transitive_in field R by A2, Def16;

now

let a, b be set ; :: thesis: ( a in field R & b in field R & [a,b] in R implies not [b,a] in R )
assume A5: ( a in field R & b in field R ) ; :: thesis: ( [a,b] in R implies not [b,a] in R )
then not [a,a] in R by A3, Def2;
hence ( [a,b] in R implies not [b,a] in R ) by A4, A5, Def8; :: thesis: verum

end;

then R is_asymmetric_in field R by Def5;
hence R is asymmetric by Def13; :: thesis: verum