set y = the Element of x;
A1: 0 + 1 < n + 1 by XREAL_1:8;

now :: thesis: card { the Element of x} c= n

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

suppose 1 c= n ; :: thesis: card { the Element of x} c= n

hence card { the Element of x} c= n by CARD_1:30; :: thesis: verum

end;

suppose A2: n in 1 ; :: thesis: card { the Element of x} c= n

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

end;

end;

end;

then { the Element of x} in Fin (x,n) ;
hence not Fin (x,n) is empty ; :: thesis: verum