let E be non empty set ; :: thesis: ( E is epsilon-transitive implies ( E |= the_axiom_of_unions iff for X being set st X in E holds

union X in E ) )

assume A1: E is epsilon-transitive ; :: thesis: ( E |= the_axiom_of_unions iff for X being set st X in E holds

union X in E )

hence ( E |= the_axiom_of_unions implies for X being set st X in E holds

union X in E ) by Th4; :: thesis: ( ( for X being set st X in E holds

union X in E ) implies E |= the_axiom_of_unions )

assume for X being set st X in E holds

union X in E ; :: thesis: E |= the_axiom_of_unions

then for u being Element of E holds union u in E ;

hence E |= the_axiom_of_unions by A1, Th4; :: thesis: verum

union X in E ) )

assume A1: E is epsilon-transitive ; :: thesis: ( E |= the_axiom_of_unions iff for X being set st X in E holds

union X in E )

hence ( E |= the_axiom_of_unions implies for X being set st X in E holds

union X in E ) by Th4; :: thesis: ( ( for X being set st X in E holds

union X in E ) implies E |= the_axiom_of_unions )

assume for X being set st X in E holds

union X in E ; :: thesis: E |= the_axiom_of_unions

then for u being Element of E holds union u in E ;

hence E |= the_axiom_of_unions by A1, Th4; :: thesis: verum