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 ) & X c= X ) ;
hence ( X is epsilon-transitive implies the_transitive-closure_of X = X ) by Th61; :: thesis: verum