theorem Th3: :: CLASSES4:3

for X being set holds
( X is axiom_GU1 iff X is epsilon-transitive )