theorem :: COHSP_1:3

for X being finite subset-closed set holds Sub_of_Fin X = X