theorem :: WELLORD2:20

for X being set holds RelIncl X is_transitive_in X