let x1, x2 be object ; :: thesis: ( x1 <> x2 implies card {x1,x2} = 2 )
A1: ( card {x1} = 1 & card {x2} = 1 ) by CARD_1:30;
A2: ( {x1,x2} = {x1} \/ {x2} & 1 + 1 = 2 ) by ENUMSET1:1;
assume x1 <> x2 ; :: thesis: card {x1,x2} = 2
hence card {x1,x2} = 2 by A1, A2, Th39, ZFMISC_1:11; :: thesis: verum