theorem Th17: :: WELLORD1:17

for Y being set
for R being Relation st R is transitive holds
R |_2 Y is transitive