theorem :: FINSUB_1:16

for A being set
for X being Element of Fin A holds X is Subset of A by Def5;