theorem :: CLASSES1:59
for X being set holds the_transitive-closure_of (the_transitive-closure_of X) = the_transitive-closure_of X by Th55;