set X = {0};
set r = {} [:{0},{0}:];
take R = RelStr(# {0},({} [:{0},{0}:]) #); :: thesis: ( R is asymmetric & R is transitive & not R is empty )
thus R is asymmetric :: thesis: ( R is transitive & not R is empty )

proof

let a be object ; :: according to RELAT_2:def 5,OPOSET_1:def 9 :: thesis: for b₁ being object holds
( not a in the carrier of R or not b₁ in the carrier of R or not [a,b₁] in the InternalRel of R or not [b₁,a] in the InternalRel of R )
let b be object ; :: thesis: ( not a in the carrier of R or not b in the carrier of R or not [a,b] in the InternalRel of R or not [b,a] in the InternalRel of R )
assume ( a in the carrier of R & b in the carrier of R ) ; :: thesis: ( not [a,b] in the InternalRel of R or not [b,a] in the InternalRel of R )
thus ( not [a,b] in the InternalRel of R or not [b,a] in the InternalRel of R ) ; :: thesis: verum

end;

thus R is transitive :: thesis: not R is empty

proof

let a be object ; :: according to RELAT_2:def 8,ORDERS_2:def 3 :: thesis: for b₁, b₂ being object holds
( not a in the carrier of R or not b₁ in the carrier of R or not b₂ in the carrier of R or not [a,b₁] in the InternalRel of R or not [b₁,b₂] in the InternalRel of R or [a,b₂] in the InternalRel of R )
thus for b₁, b₂ being object holds
( not a in the carrier of R or not b₁ in the carrier of R or not b₂ in the carrier of R or not [a,b₁] in the InternalRel of R or not [b₁,b₂] in the InternalRel of R or [a,b₂] in the InternalRel of R ) ; :: thesis: verum

end;

thus not R is empty ; :: thesis: verum