for X being set
for P being finite without_zero Subset of NAT holds (Sgm P) " X is finite without_zero Subset of NAT