let X be set ; :: thesis: ( X is epsilon-transitive implies union X c= X )
assume A1: for Y being set st Y in X holds
Y c= X ; :: according to ORDINAL1:def 2 :: thesis: union X c= X
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union X or x in X )
assume x in union X ; :: thesis: x in X
then consider Y being set such that
A2: x in Y and
A3: Y in X by TARSKI:def 4;
Y c= X by A1, A3;
hence x in X by A2; :: thesis: verum