theorem :: CARD_2:60

for X being set st card X = 2 holds
ex x, y being object st
( x <> y & X = {x,y} )