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