let A, e be set ; :: thesis: ( e in TWOELEMENTSETS A iff ( e is finite Subset of A & ex x, y being set st
( x in A & y in A & x <> y & e = {x,y} ) ) )

hereby :: thesis: ( e is finite Subset of A & ex x, y being set st
( x in A & y in A & x <> y & e = {x,y} ) implies e in TWOELEMENTSETS A )

assume e in TWOELEMENTSETS A ; :: thesis: ( e is finite Subset of A & ex x, y being set st
( x in A & y in A & x <> y & e = {x,y} ) )
then consider z being finite Subset of A such that
A1: ( e = z & card z = 2 ) ;
thus e is finite Subset of A by A1; :: thesis: ex x, y being set st
( x in A & y in A & x <> y & e = {x,y} )
reconsider e' = e as finite Subset of A by A1;
consider x, y being set such that
A2: ( x <> y & e' = {x,y} ) by A1, CARD_2:79;
take x = x; :: thesis: ex y being set st
( x in A & y in A & x <> y & e = {x,y} )
take y = y; :: thesis: ( x in A & y in A & x <> y & e = {x,y} )
( x in e' & y in e' ) by A2, TARSKI:def 2;
hence ( x in A & y in A ) ; :: thesis: ( x <> y & e = {x,y} )
thus ( x <> y & e = {x,y} ) by A2; :: thesis: verum

end;

assume ( e is finite Subset of A & ex x, y being set st
( x in A & y in A & x <> y & e = {x,y} ) ) ; :: thesis: e in TWOELEMENTSETS A
then consider x, y being Element of A such that
A3: ( x in A & y in A & not x = y & e = {x,y} ) ;
reconsider xy = {x,y} as finite Subset of A by A3, ZFMISC_1:38;
ex z being finite Subset of A st
( e = z & card z = 2 )

proof

take xy ; :: thesis: ( e = xy & card xy = 2 )
thus e = xy by A3; :: thesis: card xy = 2
thus card xy = 2 by A3, CARD_2:76; :: thesis: verum

end;

hence e in TWOELEMENTSETS A ; :: thesis: verum