reconsider A = {1,2} as non empty set ;
take A ; :: thesis: ex x1, x2 being set st
( A = {x1,x2} & x1 <> x2 )
thus ex x1, x2 being set st
( A = {x1,x2} & x1 <> x2 ) ; :: thesis: verum