:: deftheorem defines with_missing_variables ABCMIZ_1:def 55 :
for S being ManySortedSign
for X being ManySortedSet of the carrier of S holds
( X is with_missing_variables iff X " {{}} c= rng the ResultSort of S );