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

assume A1: R is empty ; :: thesis: ( 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 ; :: according to RELAT_2:def 2,RELAT_2:def 10 :: thesis: ( 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; :: according to RELAT_2:def 5,RELAT_2:def 13 :: thesis: 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; :: according to RELAT_2:def 8,RELAT_2:def 16 :: thesis: verum

assume A1: R is empty ; :: thesis: ( 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 ; :: according to RELAT_2:def 2,RELAT_2:def 10 :: thesis: ( 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; :: according to RELAT_2:def 5,RELAT_2:def 13 :: thesis: 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; :: according to RELAT_2:def 8,RELAT_2:def 16 :: thesis: verum