let X be set ; :: thesis: ( X is epsilon-transitive implies the_transitive-closure_of X = X )
for Z being set st X c= Z & Z is epsilon-transitive holds
X c= Z ;
hence ( X is epsilon-transitive implies the_transitive-closure_of X = X ) by Th54; :: thesis: verum