let x1, x2 be object ; :: thesis: card {x1,x2} <= 2
A1: ( {x1,x2} = {x1} \/ {x2} & 1 + 1 = 2 ) by ENUMSET1:1;
( card {x1} = 1 & card {x2} = 1 ) by CARD_1:30;
hence card {x1,x2} <= 2 by A1, Th42; :: thesis: verum