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 b1 being object holds
( not a in field r or not b1 in field r or not [a,b1] in r or not [b1,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 b1, b2 being object holds
( not a in field r or not b1 in field r or not b2 in field r or not [a,b1] in r or not [b1,b2] in r or [a,b2] in r )
thus for b1, b2 being object holds
( not a in field r or not b1 in field r or not b2 in field r or not [a,b1] in r or not [b1,b2] in r or [a,b2] in r ) ; :: thesis: verum
end;