theorem Th52: :: CLASSES1:52

for X being set holds X c= the_transitive-closure_of X