for X being set holds X c= the_transitive-closure_of X