let x1, x2 be set ; :: thesis: card {x1,x2} <= 2
( card {x1} = 1 & card {x2} = 1 & {x1,x2} = {x1} \/ {x2} & {x1} is finite & {x2} is finite & 1 + 1 = 2 ) by CARD_1:50, ENUMSET1:41;
hence card {x1,x2} <= 2 by Th62; :: thesis: verum