let S be ManySortedSign ; :: thesis: for X, Y being ManySortedSet of st X c= Y & X is with_missing_variables holds
Y is with_missing_variables
let X, Y be ManySortedSet of ; :: thesis: ( X c= Y & X is with_missing_variables implies Y is with_missing_variables )
assume that
Z0: X c= Y and
Z1: X " {{} } c= rng the ResultSort of S ; :: according to ABCMIZ_1:def 55 :: thesis: Y is with_missing_variables
let x be set ; :: according to TARSKI:def 3,ABCMIZ_1:def 55 :: thesis: ( not x in Y " {{} } or x in rng the ResultSort of S )
assume x in Y " {{} } ; :: thesis: x in rng the ResultSort of S
then A0: ( x in dom Y & Y . x in {{} } & dom Y = the carrier of S & dom X = the carrier of S ) by FUNCT_1:def 13, PARTFUN1:def 4;
then ( Y . x = {} & X . x c= Y . x ) by Z0, PBOOLE:def 5, TARSKI:def 1;
then X . x = {} ;
then X . x in {{} } by TARSKI:def 1;
then x in X " {{} } by A0, FUNCT_1:def 13;
hence x in rng the ResultSort of S by Z1; :: thesis: verum