let X be set ; :: thesis: ( X is axiom_GU1 iff X is epsilon-transitive )

hereby :: thesis: ( X is epsilon-transitive implies X is axiom_GU1 )

assume X is axiom_GU1 ; :: thesis: X is epsilon-transitive
then for x being set st x in X holds
x c= X ;
hence X is epsilon-transitive ; :: thesis: verum

end;

assume A1: X is epsilon-transitive ; :: thesis: X is axiom_GU1

now :: thesis: for x, y being set st y in x & x in X holds
y in X

let x, y be set ; :: thesis: ( y in x & x in X implies y in X )
assume that
A2: y in x and
A3: x in X ; :: thesis: y in X
x c= X by A3, A1;
hence y in X by A2; :: thesis: verum

end;

hence X is axiom_GU1 ; :: thesis: verum