let x1, x2, x3 be set ; :: thesis: ( x1 <> x2 & x1 <> x3 & x2 <> x3 implies card {x1,x2,x3} = 3 )
assume ( x1 <> x2 & x1 <> x3 & x2 <> x3 ) ; :: thesis: card {x1,x2,x3} = 3
then ( card {x1,x2} = 2 & not x3 in {x1,x2} & {x1,x2} is finite & {x1,x2,x3} = {x1,x2} \/ {x3} ) by Th76, ENUMSET1:43, TARSKI:def 2;
hence card {x1,x2,x3} = 2 + 1 by Th54
.= 3 ;
:: thesis: verum