let x1, x2, x3 be object ; ( x1 <> x2 & x1 <> x3 & x2 <> x3 implies card {x1,x2,x3} = 3 )
assume
( x1 <> x2 & x1 <> x3 & x2 <> x3 )
; card {x1,x2,x3} = 3
then A1:
( card {x1,x2} = 2 & not x3 in {x1,x2} )
by Th56, TARSKI:def 2;
{x1,x2,x3} = {x1,x2} \/ {x3}
by ENUMSET1:3;
hence card {x1,x2,x3} =
2 + 1
by A1, Th40
.=
3
;
verum