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