theorem Th58: :: CLASSES1:58

for X, Y being set st X c= Y holds
the_transitive-closure_of X c= the_transitive-closure_of Y