theorem Th16: :: NUMBER09:16

for a being Nat
for X being included_in_Seg set st a in X holds
a divides Product (Sgm X)