theorem :: OSAFREE:29

for S being locally_directed OrderSortedSign
for X being non-empty ManySortedSet of S holds PTVars X is non-empty