let X be set ; :: thesis: Fin X is semiring_of_sets of X
Fin X c= bool X by FINSUB_1:13;
then Fin X is Subset-Family of X ;
hence Fin X is semiring_of_sets of X ; :: thesis: verum