consider y being Element of x;
A1: 0 + 1 < n + 1 by XREAL_1:10;

now

per cases ( 1 c= n or n in 1 ) by ORDINAL1:26;

suppose 1 c= n ; :: thesis: card {y} c= n

hence card {y} c= n by CARD_1:50; :: thesis: verum

end;

suppose A2: n in 1 ; :: thesis: card {y} c= n

1 = { k where k is Element of NAT : k < 1 } by AXIOMS:30;
then ex k being Element of NAT st
( k = n & k < 1 ) by A2;
hence card {y} c= n by A1, NAT_1:13; :: thesis: verum

end;

end;

end;

then {y} in Fin x,n ;
hence not Fin x,n is empty ; :: thesis: verum