theorem :: CLASSES1:51

for X being set holds the_transitive-closure_of X is epsilon-transitive ;