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