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

hereby :: thesis: ( e is finite Subset of A & ex x, y being object 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 object st
( x in A & y in A & x <> y & e = {x,y} ) )
then A1: ex z being Subset of A st
( e = z & card z = 2 ) ;
then reconsider e9 = e as finite Subset of A ;
thus e is finite Subset of A by A1; :: thesis: ex x, y being object st
( x in A & y in A & x <> y & e = {x,y} )
consider x, y being object such that
A2: x <> y and
A3: e9 = {x,y} by A1, CARD_2:60;
take x = x; :: thesis: ex y being object 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 e9 & y in e9 ) by A3, TARSKI:def 2;
hence ( x in A & y in A ) ; :: thesis: ( x <> y & e = {x,y} )
thus ( x <> y & e = {x,y} ) by A2, A3; :: thesis: verum

end;

assume that
e is finite Subset of A and
A4: ex x, y being object st
( x in A & y in A & x <> y & e = {x,y} ) ; :: thesis: e in TWOELEMENTSETS A
consider x, y being Element of A such that
A5: x in A and
y in A and
A6: not x = y and
A7: e = {x,y} by A4;
reconsider xy = {x,y} as finite Subset of A by A5, ZFMISC_1:32;
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 A7; :: thesis: card xy = 2
thus card xy = 2 by A6, CARD_2:57; :: thesis: verum

end;

hence e in TWOELEMENTSETS A ; :: thesis: verum