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