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