let x1, x2, x3, x4, x5, x6 be object ; card {x1,x2,x3,x4,x5,x6} <= 6
card {x2,x3,x4,x5,x6} <= 5
by Th52;
then A1:
1 + (card {x2,x3,x4,x5,x6}) <= 1 + 5
by XREAL_1:7;
( card {x1} = 1 & {x1,x2,x3,x4,x5,x6} = {x1} \/ {x2,x3,x4,x5,x6} )
by CARD_1:30, ENUMSET1:11;
then
card {x1,x2,x3,x4,x5,x6} <= 1 + (card {x2,x3,x4,x5,x6})
by Th42;
hence
card {x1,x2,x3,x4,x5,x6} <= 6
by A1, XXREAL_0:2; verum