let R be Relation; ( 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
; RELAT_2:def 10,RELAT_2:def 16 R is asymmetric
let a be object ; RELAT_2:def 5,RELAT_2:def 13 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 ; ( 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
; ( 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; verum