let A be 2 -element set ; :: thesis: ex a, b being Element of A st
( a <> b & A = {a,b} )
card A = 2 by CARD_1:def 7;
then consider c, d being object such that
A1: ( c <> d & A = {c,d} ) by CARD_2:60;
( c in A & d in A ) by A1, TARSKI:def 2;
hence ex a, b being Element of A st
( a <> b & A = {a,b} ) by A1; :: thesis: verum