let X be ManySortedSet of the carrier of S; :: thesis: ( X is non-empty implies X is with_missing_variables )
assume A1: X is non-empty ; :: thesis: X is with_missing_variables
let x be object ; :: according to TARSKI:def 3,ABCMIZ_1:def 55 :: thesis: ( not x in X " {{}} or x in rng the ResultSort of S )
assume A2: x in X " {{}} ; :: thesis: x in rng the ResultSort of S
then A3: x in dom X by FUNCT_1:def 7;
A4: X . x in {{}} by A2, FUNCT_1:def 7;
A5: X . x in rng X by A3, FUNCT_1:def 3;
X . x = {} by A4, TARSKI:def 1;
hence x in rng the ResultSort of S by A1, A5; :: thesis: verum