set X = I;
take r = {} [:I,I:]; :: thesis: ( r is asymmetric & r is transitive )
thus r is asymmetric :: thesis: r is transitive

proof

let a be object ; :: according to RELAT_2:def 5,RELAT_2:def 13 :: thesis: for b₁ being object holds
( not a in field r or not b₁ in field r or not [a,b₁] in r or not [b₁,a] in r )
let b be object ; :: thesis: ( not a in field r or not b in field r or not [a,b] in r or not [b,a] in r )
thus ( not a in field r or not b in field r or not [a,b] in r or not [b,a] in r ) ; :: thesis: verum

end;

thus r is transitive :: thesis: verum

proof

let a be object ; :: according to RELAT_2:def 8,RELAT_2:def 16 :: thesis: for b₁, b₂ being object holds
( not a in field r or not b₁ in field r or not b₂ in field r or not [a,b₁] in r or not [b₁,b₂] in r or [a,b₂] in r )
thus for b₁, b₂ being object holds
( not a in field r or not b₁ in field r or not b₂ in field r or not [a,b₁] in r or not [b₁,b₂] in r or [a,b₂] in r ) ; :: thesis: verum

end;