for n being non zero Nat
for p being RelStr-yielding ManySortedSet of n holds
( not product p is empty iff p is non-Empty )