let x1, x2, x3, x4, x5 be object ; ( x1,x2,x3,x4,x5 are_mutually_distinct implies card {x1,x2,x3,x4,x5} = 5 )
A1:
{x1,x2,x3,x4,x5} = {x1,x2,x3,x4} \/ {x5}
by ENUMSET1:10;
assume A2:
x1,x2,x3,x4,x5 are_mutually_distinct
; card {x1,x2,x3,x4,x5} = 5
then A3:
( x3 <> x5 & x4 <> x5 )
by ZFMISC_1:def 7;
A4:
( x2 <> x4 & x3 <> x4 )
by A2, ZFMISC_1:def 7;
A5:
( x1 <> x4 & x2 <> x3 )
by A2, ZFMISC_1:def 7;
( x1 <> x5 & x2 <> x5 )
by A2, ZFMISC_1:def 7;
then A6:
not x5 in {x1,x2,x3,x4}
by A3, ENUMSET1:def 2;
( x1 <> x2 & x1 <> x3 )
by A2, ZFMISC_1:def 7;
then
card {x1,x2,x3,x4} = 4
by A5, A4, Th58;
hence card {x1,x2,x3,x4,x5} =
4 + 1
by A6, A1, Th40
.=
5
;
verum