let x1, x2, x3, x4, x5 be set ; :: thesis: ( x1,x2,x3,x4,x5 are_mutually_different implies card {x1,x2,x3,x4,x5} = 5 )
assume x1,x2,x3,x4,x5 are_mutually_different ; :: thesis: card {x1,x2,x3,x4,x5} = 5
then ( x1 <> x2 & x1 <> x3 & x1 <> x4 & x1 <> x5 & x2 <> x3 & x2 <> x4 & x2 <> x5 & x3 <> x4 & x3 <> x5 & x4 <> x5 ) by ZFMISC_1:def 7;
then ( card {x1,x2,x3,x4} = 4 & not x5 in {x1,x2,x3,x4} & {x1,x2,x3,x4} is finite & {x1,x2,x3,x4,x5} = {x1,x2,x3,x4} \/ {x5} ) by Th78, ENUMSET1:50, ENUMSET1:def 2;
hence card {x1,x2,x3,x4,x5} = 4 + 1 by Th54
.= 5 ;
:: thesis: verum