for X being set holds the_transitive-closure_of X is epsilon-transitive ;