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