theorem Th54: :: CLASSES1:54

for X, Y being set st ( for Z being set st X c= Z & Z is epsilon-transitive holds
Y c= Z ) & X c= Y & Y is epsilon-transitive holds
the_transitive-closure_of X = Y by Th53, Th52;