theorem Th23: :: CLASSES1:23

for X being set st X is epsilon-transitive holds
Tarski-Class X is epsilon-transitive