theorem Th42: :: NAT_4:43

for X1 being set
for X2 being finite set st X1 c= X2 & X2 c= NAT & not {} in X2 holds
Product (Sgm X1) <= Product (Sgm X2)