theorem :: ORDERS_1:80

for R being Relation
for X being set st R is_transitive_in X holds
R ~ is_transitive_in X by Lm13;