for A, e being set holds
( 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} ) ) )