let X be ManySortedSet of ; :: thesis: ( X is non-empty implies X is with_missing_variables )
assume A0: X is non-empty ; :: thesis: X is with_missing_variables
let x be set ; :: according to TARSKI:def 3,ABCMIZ_1:def 55 :: thesis: ( not x in X " {{} } or x in rng the ResultSort of S )
assume x in X " {{} } ; :: thesis: x in rng the ResultSort of S
then ( x in dom X & X . x in {{} } ) by FUNCT_1:def 13;
then ( X . x in rng X & X . x = {} ) by FUNCT_1:def 5, TARSKI:def 1;
hence x in rng the ResultSort of S by A0, RELAT_1:def 9; :: thesis: verum