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

assume that

A1: R is_irreflexive_in field R and

A2: R is_transitive_in field R ; :: according to RELAT_2:def 10,RELAT_2:def 16 :: thesis: R is asymmetric

let a be object ; :: according to RELAT_2:def 5,RELAT_2:def 13 :: thesis: for y being object st a in field R & y in field R & [a,y] in R holds

not [y,a] in R

let b be object ; :: thesis: ( a in field R & b in field R & [a,b] in R implies not [b,a] in R )

assume that

A3: a in field R and

A4: b in field R ; :: thesis: ( not [a,b] in R or not [b,a] in R )

not [a,a] in R by A1, A3;

hence ( not [a,b] in R or not [b,a] in R ) by A2, A3, A4; :: thesis: verum

assume that

A1: R is_irreflexive_in field R and

A2: R is_transitive_in field R ; :: according to RELAT_2:def 10,RELAT_2:def 16 :: thesis: R is asymmetric

let a be object ; :: according to RELAT_2:def 5,RELAT_2:def 13 :: thesis: for y being object st a in field R & y in field R & [a,y] in R holds

not [y,a] in R

let b be object ; :: thesis: ( a in field R & b in field R & [a,b] in R implies not [b,a] in R )

assume that

A3: a in field R and

A4: b in field R ; :: thesis: ( not [a,b] in R or not [b,a] in R )

not [a,a] in R by A1, A3;

hence ( not [a,b] in R or not [b,a] in R ) by A2, A3, A4; :: thesis: verum