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

{X,Y} in E ) )

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

{X,Y} in E )

hence ( E |= the_axiom_of_pairs implies for X, Y being set st X in E & Y in E holds

{X,Y} in E ) by Th2; :: thesis: ( ( for X, Y being set st X in E & Y in E holds

{X,Y} in E ) implies E |= the_axiom_of_pairs )

assume for X, Y being set st X in E & Y in E holds

{X,Y} in E ; :: thesis: E |= the_axiom_of_pairs

then for u, v being Element of E holds {u,v} in E ;

hence E |= the_axiom_of_pairs by A1, Th2; :: thesis: verum

{X,Y} in E ) )

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

{X,Y} in E )

hence ( E |= the_axiom_of_pairs implies for X, Y being set st X in E & Y in E holds

{X,Y} in E ) by Th2; :: thesis: ( ( for X, Y being set st X in E & Y in E holds

{X,Y} in E ) implies E |= the_axiom_of_pairs )

assume for X, Y being set st X in E & Y in E holds

{X,Y} in E ; :: thesis: E |= the_axiom_of_pairs

then for u, v being Element of E holds {u,v} in E ;

hence E |= the_axiom_of_pairs by A1, Th2; :: thesis: verum