theorem :: CLASSES1:57

for A being Ordinal holds the_transitive-closure_of A = A by Th55;