theorem :: FINSUB_1:17

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