theorem :: PBOOLE:112

for I being set
for X being ManySortedSet of I st X <> EmptyMS I holds
X meets X