theorem Th117: :: ABCMIZ_1:117

for S being ManySortedSign
for X, Y being ManySortedSet of the carrier of S st X c= Y & X is with_missing_variables holds
Y is with_missing_variables