:: deftheorem defines Fin BAGORDER:def 2 :
for x being non empty set
for n being non zero Element of NAT holds Fin (x,n) = { y where y is Subset of x : ( y is finite & not y is empty & card y c= n ) } ;