theorem Th55: :: CLASSES1:55

for X being set st X is epsilon-transitive holds
the_transitive-closure_of X = X