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