let R be Relation; ( R is empty implies ( R is irreflexive & R is asymmetric & R is transitive ) )
assume A1:
R is empty
; ( R is irreflexive & R is asymmetric & R is transitive )
hence
for x being object st x in field R holds
not [x,x] in R
; RELAT_2:def 2,RELAT_2:def 10 ( R is asymmetric & R is transitive )
thus
for x, y being object st x in field R & y in field R & [x,y] in R holds
not [y,x] in R
by A1; RELAT_2:def 5,RELAT_2:def 13 R is transitive
thus
for x, y, z being object st x in field R & y in field R & z in field R & [x,y] in R & [y,z] in R holds
[x,z] in R
by A1; RELAT_2:def 8,RELAT_2:def 16 verum