set y = the Element of x;

A1: 0 + 1 < n + 1 by XREAL_1:8;

hence not Fin (x,n) is empty ; :: thesis: verum

A1: 0 + 1 < n + 1 by XREAL_1:8;

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

then
{ the Element of x} in Fin (x,n)
;end;

hence not Fin (x,n) is empty ; :: thesis: verum