:: deftheorem Def2 defines epsilon-transitive ORDINAL1:def 2 :
for X being set holds
( X is epsilon-transitive iff for x being set st x in X holds
x c= X );