theorem Th107: :: PBOOLE:107

for I being set
for X, Y, Z being ManySortedSet of I st X meets Y & Y c= Z holds
X meets Z