let x1, x2, x3, x4 be object ; ( 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 )
; card {x1,x2,x3,x4} = 4
then A1:
( card {x1,x2,x3} = 3 & not x4 in {x1,x2,x3} )
by Th57, ENUMSET1:def 1;
{x1,x2,x3,x4} = {x1,x2,x3} \/ {x4}
by ENUMSET1:6;
hence card {x1,x2,x3,x4} =
3 + 1
by A1, Th40
.=
4
;
verum