for X, Y being set st X c= Y & Y is epsilon-transitive holds
the_transitive-closure_of X c= Y