let X, Y be set ; :: thesis: ( ( for Z being set st X c= Z & Z is epsilon-transitive holds
Y c= Z ) & X c= Y & Y is epsilon-transitive implies the_transitive-closure_of X = Y )
assume A1: for Z being set st X c= Z & Z is epsilon-transitive holds
Y c= Z ; :: thesis: ( not X c= Y or not Y is epsilon-transitive or the_transitive-closure_of X = Y )
assume ( X c= Y & Y is epsilon-transitive ) ; :: thesis: the_transitive-closure_of X = Y
hence the_transitive-closure_of X c= Y by Th60; :: according to XBOOLE_0:def 10 :: thesis: Y c= the_transitive-closure_of X
( the_transitive-closure_of X is epsilon-transitive & X c= the_transitive-closure_of X ) by Th58, Th59;
hence Y c= the_transitive-closure_of X by A1; :: thesis: verum