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