theorem :: SRINGS_2:6
for X being set holds Fin X is semiring_of_sets of X by FINSUB_1:13;